src/Pure/Isar/isar_syn.ML
changeset 23865 3ea92c014a3e
parent 23795 b094f9b7a52d
child 23989 d7df8545f9f6
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 19 23:18:50 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 19 23:18:51 2007 +0200
@@ -897,18 +897,10 @@
   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
 
-val use_thy_onlyP =
-  OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
-    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only));
-
 val update_thyP =
   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
 
-val update_thy_onlyP =
-  OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
-    K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only));
-
 val touch_thyP =
   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
@@ -1026,9 +1018,9 @@
   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
   print_termP, print_typeP, print_codesetupP,
   (*system commands*)
-  cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
-  touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
-  kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
-  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
+  cdP, pwdP, use_thyP, update_thyP, touch_thyP, touch_all_thysP,
+  touch_child_thysP, remove_thyP, kill_thyP, display_draftsP,
+  print_draftsP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
+  init_toplevelP, welcomeP];
 
 end;