src/Pure/proof_general.ML
changeset 21350 6e58289b6685
parent 20951 868120282837
child 21464 abaf43b011ee
--- a/src/Pure/proof_general.ML	Tue Nov 14 00:15:37 2006 +0100
+++ b/src/Pure/proof_general.ML	Tue Nov 14 00:15:38 2006 +0100
@@ -1377,12 +1377,12 @@
 
 val context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
-    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
+    (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only));
 
 val try_context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
     (P.name >> (Toplevel.no_timing oo
-      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
+      (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only)));
 
 val restartP =
   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control