# HG changeset patch
# User wenzelm
# Date 927296628 -7200
# Node ID 335833a8b10a50b690f008389d82379eb339a7fc
# Parent  fec75b36a8090f0ecea813513268cb64795a04f8
added use_thy_only;

diff -r fec75b36a809 -r 335833a8b10a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri May 21 16:23:18 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri May 21 16:23:48 1999 +0200
@@ -22,6 +22,7 @@
   val cd: string -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val use_thy: string -> Toplevel.transition -> Toplevel.transition
+  val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
   val update_thy: string -> Toplevel.transition -> Toplevel.transition
   val print_theory: Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
@@ -97,6 +98,7 @@
 (* load theory files *)
 
 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
+fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
 
 
diff -r fec75b36a809 -r 335833a8b10a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri May 21 16:23:18 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri May 21 16:23:48 1999 +0200
@@ -457,6 +457,10 @@
   OuterSyntax.improper_command "use_thy" "use theory file"
     (name >> IsarCmd.use_thy);
 
+val use_thy_onlyP =
+  OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
+    (name >> IsarCmd.use_thy_only);
+
 val update_thyP =
   OuterSyntax.improper_command "update_thy" "update theory file"
     (name >> IsarCmd.update_thy);
@@ -522,8 +526,8 @@
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)
-  cdP, pwdP, use_thyP, update_thyP, prP, commitP, quitP, exitP,
-  restartP, breakP];
+  cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
+  quitP, exitP, restartP, breakP];
 
 
 end;