# HG changeset patch
# User wenzelm
# Date 930842669 -7200
# Node ID 850812ed9976755e531204597d413bd9148a84e8
# Parent  27ba88d573993dae79d973413d8f1583a4440866
fix, assume, presume: prf_asm;

diff -r 27ba88d57399 -r 850812ed9976 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 01 17:24:14 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 01 17:24:29 1999 +0200
@@ -288,17 +288,17 @@
 (* proof context *)
 
 val assumeP =
-  OuterSyntax.command "assume" "assume propositions" K.prf_decl
+  OuterSyntax.command "assume" "assume propositions" K.prf_asm
     ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
 
 val presumeP =
-  OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_decl
+  OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
     ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
 
 val fixP =
-  OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
+  OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));