src/Pure/Isar/isar_syn.ML
changeset 19844 2c1fdc397ded
parent 19809 b8f35de1c664
child 20305 16c8f44b1852
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Jun 11 21:59:23 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 11 21:59:24 2006 +0200
     1.3 @@ -449,7 +449,7 @@
     1.4  val fixP =
     1.5    OuterSyntax.command "fix" "fix local variables (Skolem constants)"
     1.6      (K.tag_proof K.prf_asm)
     1.7 -    (P.simple_fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
     1.8 +    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
     1.9  
    1.10  val assumeP =
    1.11    OuterSyntax.command "assume" "assume propositions"
    1.12 @@ -465,19 +465,20 @@
    1.13    OuterSyntax.command "def" "local definition"
    1.14      (K.tag_proof K.prf_asm)
    1.15      (P.and_list1
    1.16 -      (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
    1.17 +      (P.opt_thm_name ":" --
    1.18 +        ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
    1.19      >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
    1.20  
    1.21  val obtainP =
    1.22    OuterSyntax.command "obtain" "generalized existence"
    1.23      (K.tag_proof K.prf_asm_goal)
    1.24 -    (P.parname -- Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- P.statement
    1.25 +    (P.parname -- Scan.optional (P.fixes --| P.$$$ "where") [] -- P.statement
    1.26        >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
    1.27  
    1.28  val guessP =
    1.29    OuterSyntax.command "guess" "wild guessing (unstructured)"
    1.30      (K.tag_proof K.prf_asm_goal)
    1.31 -    (Scan.optional P.simple_fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
    1.32 +    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
    1.33  
    1.34  val letP =
    1.35    OuterSyntax.command "let" "bind text variables"