continue

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13615 3260e6d1-4efc-4170-b0a7-36055960796d

C11-FrontEnd/src/C_Model_ml.thy

@@ -394,13 +394,13 @@ section \<open>Loading of Generated Grammar\<close>
 
 ML\<open>datatype antiq_head = Setup | Hook of Symbol_Pos.T list\<close>
 
-ML_file "../mlton/lib/mlyacc-lib/base.sig"
-ML_file "../mlton/lib/mlyacc-lib/join.sml"
-ML_file "../mlton/lib/mlyacc-lib/lrtable.sml"
-ML_file "../mlton/lib/mlyacc-lib/stream.sml"
+ML_file "../copied_from_git/mlton/lib/mlyacc-lib/base.sig"
+ML_file "../copied_from_git/mlton/lib/mlyacc-lib/join.sml"
+ML_file "../copied_from_git/mlton/lib/mlyacc-lib/lrtable.sml"
+ML_file "../copied_from_git/mlton/lib/mlyacc-lib/stream.sml"
 (*ML\<open>val foldl = List.foldl val foldr = List.foldr\<close>
-  ML_file "../mlton/lib/mlyacc-lib/parser2.sml"*)
-ML_file "../mlton/lib/mlyacc-lib/parser1.sml"
+  ML_file "../copied_from_git/mlton/lib/mlyacc-lib/parser2.sml"*)
+ML_file "../copied_from_git/mlton/lib/mlyacc-lib/parser1.sml"
 ML_file "../generated/language_c.grm.sig"
 ML_file "../generated/language_c.grm.sml"
 

C11-FrontEnd/src/C_Model_ml_lex.thy

@@ -1142,7 +1142,7 @@ end;
 \<close>
 
 section \<open>Instantiation of the Parser with the Lexer\<close>
-text\<open>The parser consists of a generic module @{file "../mlton/lib/mlyacc-lib/base.sig"}, 
+text\<open>The parser consists of a generic module @{file "../copied_from_git/mlton/lib/mlyacc-lib/base.sig"}, 
 which interprets a automata-like format generated from smlyacc.\<close>
 
 ML\<open>