Present.token_source after load (better errors!?);
authorwenzelm
Thu, 07 Oct 1999 12:36:39 +0200
changeset 7774 6da9b544a12d
parent 7773 ce86227f29d0
child 7775 26898fbd19ca
Present.token_source after load (better errors!?);
src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 12:33:54 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 12:36:39 1999 +0200
@@ -387,8 +387,8 @@
     Present.init_theory name;
     Present.verbatim_source name (present_text text);
     if is_old_theory (src, pos) then ThySyn.load_thy name text
-    else (Present.token_source name (present_toks text pos);
-      Toplevel.excursion_error (parse_thy (src, pos)))
+    else (Toplevel.excursion_error (parse_thy (src, pos));
+      Present.token_source name (present_toks text pos))
   end;
 
 in