1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 15:34:54 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Jul 19 17:29:35 2021 +0200
1.3 @@ -167,7 +167,7 @@
1.4 -------------------------------------------------------------------------ARE AT THE RIGHT MARGIN*)
1.5 section \<open>trials with Isabelle's functions\<close>
1.6 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.7 - ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
1.8 + ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
1.9 ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
1.10 ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
1.11 ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
1.12 @@ -329,7 +329,9 @@
1.13 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.14 ML \<open>
1.15 \<close> ML \<open>
1.16 +@{term Let}
1.17 \<close> ML \<open>
1.18 +val Const (\<^const_name>\<open>Let\<close>, _) = @{term Let}
1.19 \<close> ML \<open>
1.20 \<close> ML \<open>
1.21 \<close> ML \<open>