# HG changeset patch
# User wenzelm
# Date 947069288 -3600
# Node ID 80a3c30d088bb28dfd7aba02d680bea6935efb28
# Parent  4da940d100f5dcc32f176bec8836b5b0082eb9da
moved obtain to obtain.ML;

diff -r 4da940d100f5 -r 80a3c30d088b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jan 05 11:47:46 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 05 11:48:08 2000 +0100
@@ -409,18 +409,6 @@
     (calc_args -- P.marg_comment >> IsarThy.finally);
 
 
-(* obtain *)
-
-val obtainP =
-  OuterSyntax.command "obtain" "document-level existential quantifier (EXPERIMENTAL!)"
-    K.prf_asm_goal
-    (Scan.optional
-      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
-        --| P.$$$ "in") [] --
-      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
-    >> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain)));
-
-
 (* proof navigation *)
 
 val backP =
@@ -628,8 +616,8 @@
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
-  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, obtainP,
-  backP, cannot_undoP, clear_undosP, redoP, undos_proofP, kill_proofP, undoP,
+  skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
+  cannot_undoP, clear_undosP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,