clarified syntax;
authorwenzelm
Sat Jun 11 16:41:11 2016 +0200 (2016-06-11)
changeset 63285e9c777bfd78c
parent 63284 c20946f5b6fb
child 63286 ce90bb3d2902
clarified syntax;
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Quick_Reference.thy
src/Doc/Isar_Ref/Spec.thy
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Library/rewrite.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/inductive.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Pure.thy
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Jun 11 13:57:59 2016 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Jun 11 16:41:11 2016 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4    @{rail \<open>
     1.5      (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
     1.6        @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
     1.7 -      @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
     1.8 +      @{syntax vars} @{syntax for_fixes} \<newline>
     1.9        (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
    1.10      ;
    1.11      @@{command print_inductives} ('!'?)
     2.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Jun 11 13:57:59 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Jun 11 16:41:11 2016 +0200
     2.3 @@ -346,7 +346,9 @@
     2.4    to introduce multiple such items simultaneously.
     2.5  
     2.6    @{rail \<open>
     2.7 -    @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
     2.8 +    @{syntax_def vars}:
     2.9 +      (((@{syntax name} +) ('::' @{syntax type})? |
    2.10 +        @{syntax name} ('::' @{syntax type})? @{syntax mixfix}) + @'and')
    2.11      ;
    2.12      @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
    2.13      ;
    2.14 @@ -361,20 +363,6 @@
    2.15    another level of iteration, with explicit @{keyword_ref "and"} separators;
    2.16    e.g.\ see @{command "fix"} and @{command "assume"} in
    2.17    \secref{sec:proof-context}.
    2.18 -
    2.19 -  @{rail \<open>
    2.20 -    @{syntax_def "fixes"}:
    2.21 -      ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and')
    2.22 -    ;
    2.23 -    @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})?
    2.24 -  \<close>}
    2.25 -
    2.26 -  The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
    2.27 -  admits specification of mixfix syntax for the entities that are introduced
    2.28 -  into the context. An optional suffix ``@{keyword "for"}~\<open>fixes\<close>'' is
    2.29 -  admitted in many situations to indicate a so-called ``eigen-context'' of a
    2.30 -  formal element: the result will be exported and thus generalized over the
    2.31 -  given variables.
    2.32  \<close>
    2.33  
    2.34  
    2.35 @@ -463,6 +451,8 @@
    2.36  
    2.37  
    2.38    @{rail \<open>
    2.39 +    @{syntax_def for_fixes}: (@'for' @{syntax vars})?
    2.40 +    ;
    2.41      @{syntax_def multi_specs}: (@{syntax structured_spec} + '|')
    2.42      ;
    2.43      @{syntax_def structured_spec}:
    2.44 @@ -470,7 +460,7 @@
    2.45      ;
    2.46      @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))?
    2.47      ;
    2.48 -    @{syntax_def specification}: @{syntax "fixes"} @'where' @{syntax multi_specs}
    2.49 +    @{syntax_def specification}: @{syntax vars} @'where' @{syntax multi_specs}
    2.50    \<close>}
    2.51  \<close>
    2.52  
     3.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat Jun 11 13:57:59 2016 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sat Jun 11 16:41:11 2016 +0200
     3.3 @@ -159,7 +159,7 @@
     3.4    \<phi>[t]\<close>.
     3.5  
     3.6    @{rail \<open>
     3.7 -    @@{command fix} @{syntax "fixes"}
     3.8 +    @@{command fix} @{syntax vars}
     3.9      ;
    3.10      (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}
    3.11      ;
    3.12 @@ -167,8 +167,8 @@
    3.13      ;
    3.14      prems: (@'if' (@{syntax props'} + @'and'))?
    3.15      ;
    3.16 -    @@{command define} (@{syntax "fixes"} + @'and')
    3.17 -      @'where' (@{syntax props} + @'and') @{syntax for_fixes}
    3.18 +    @@{command define} @{syntax vars} @'where'
    3.19 +      (@{syntax props} + @'and') @{syntax for_fixes}
    3.20      ;
    3.21      @@{command def} (def + @'and')
    3.22      ;
    3.23 @@ -417,7 +417,7 @@
    3.24      ;
    3.25      @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
    3.26      ;
    3.27 -    @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where'
    3.28 +    @{syntax_def obtain_case}: @{syntax vars} @'where'
    3.29        (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
    3.30    \<close>}
    3.31  
    3.32 @@ -1335,14 +1335,14 @@
    3.33    @{rail \<open>
    3.34      @@{command consider} @{syntax obtain_clauses}
    3.35      ;
    3.36 -    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>
    3.37 +    @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>
    3.38        @'where' concl prems @{syntax for_fixes}
    3.39      ;
    3.40      concl: (@{syntax props} + @'and')
    3.41      ;
    3.42      prems: (@'if' (@{syntax props'} + @'and'))?
    3.43      ;
    3.44 -    @@{command guess} (@{syntax "fixes"} + @'and')
    3.45 +    @@{command guess} @{syntax vars}
    3.46    \<close>}
    3.47  
    3.48    \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)
     4.1 --- a/src/Doc/Isar_Ref/Quick_Reference.thy	Sat Jun 11 13:57:59 2016 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Sat Jun 11 16:41:11 2016 +0200
     4.3 @@ -15,7 +15,7 @@
     4.4      \<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
     4.5      & \<open>|\<close> & \<^theory_text>\<open>theorem name: props "proof"\<close> \\
     4.6      & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
     4.7 -    & & \quad\<^theory_text>\<open>fixes "var\<^sup>+"\<close> \\
     4.8 +    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
     4.9      & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
    4.10      & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
    4.11      \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
    4.12 @@ -23,7 +23,7 @@
    4.13      \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
    4.14      & \<open>|\<close> & \<^theory_text>\<open>supply facts\<close> \\
    4.15      & \<open>|\<close> & \<^theory_text>\<open>subgoal "proof"\<close> \\
    4.16 -    & \<open>|\<close> & \<^theory_text>\<open>subgoal for "var\<^sup>+" "proof"\<close> \\
    4.17 +    & \<open>|\<close> & \<^theory_text>\<open>subgoal for vars "proof"\<close> \\
    4.18      & \<open>|\<close> & \<^theory_text>\<open>using facts\<close> \\
    4.19      & \<open>|\<close> & \<^theory_text>\<open>unfolding facts\<close> \\
    4.20      \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
    4.21 @@ -31,14 +31,14 @@
    4.22      & \<open>|\<close> & \<^theory_text>\<open>note name = facts\<close> \\
    4.23      & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
    4.24      & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
    4.25 -    & \<open>|\<close> & \<^theory_text>\<open>fix "var\<^sup>+"\<close> \\
    4.26 +    & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
    4.27      & \<open>|\<close> & \<^theory_text>\<open>assume name: props\<close> \\
    4.28 -    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for "var\<^sup>+"\<close> \\
    4.29 +    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\
    4.30      & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
    4.31      \<open>goal\<close> & = & \<^theory_text>\<open>have name: props "proof"\<close> \\
    4.32 -    & \<open>|\<close> & \<^theory_text>\<open>have name: props if name: props for "var\<^sup>+" "proof"\<close> \\
    4.33 +    & \<open>|\<close> & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
    4.34      & \<open>|\<close> & \<^theory_text>\<open>show name: props "proof"\<close> \\
    4.35 -    & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for "var\<^sup>+" "proof"\<close> \\
    4.36 +    & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
    4.37    \end{tabular}
    4.38  \<close>
    4.39  
     5.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Jun 11 13:57:59 2016 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Jun 11 16:41:11 2016 +0200
     5.3 @@ -354,7 +354,7 @@
     5.4    \end{matharray}
     5.5  
     5.6    @{rail \<open>
     5.7 -    @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
     5.8 +    @@{command axiomatization} @{syntax vars}? (@'where' axiomatization)?
     5.9      ;
    5.10      axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
    5.11        @{syntax spec_prems} @{syntax for_fixes}
    5.12 @@ -516,7 +516,7 @@
    5.13        @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
    5.14      ;
    5.15      @{syntax_def context_elem}:
    5.16 -      @'fixes' @{syntax "fixes"} |
    5.17 +      @'fixes' @{syntax vars} |
    5.18        @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
    5.19        @'assumes' (@{syntax props} + @'and') |
    5.20        @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
     6.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Jun 11 13:57:59 2016 +0200
     6.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Jun 11 16:41:11 2016 +0200
     6.3 @@ -400,7 +400,7 @@
     6.4  
     6.5  val _ =
     6.6    Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
     6.7 -    (Parse.fixes -- (Parse.where_ |-- Parse.!!! multi_specs')
     6.8 -      >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
     6.9 +    (Parse.vars -- (Parse.where_ |-- Parse.!!! multi_specs')
    6.10 +      >> (fn (vars, specs) => add_fixrec_cmd vars specs))
    6.11  
    6.12  end
     7.1 --- a/src/HOL/Library/rewrite.ML	Sat Jun 11 13:57:59 2016 +0200
     7.2 +++ b/src/HOL/Library/rewrite.ML	Sat Jun 11 16:41:11 2016 +0200
     7.3 @@ -333,7 +333,7 @@
     7.4          val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
     7.5          val atom =  (Args.$$$ "asm" >> K Asm) ||
     7.6            (Args.$$$ "concl" >> K Concl) ||
     7.7 -          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) ||
     7.8 +          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) ||
     7.9            (Parse.term >> Term)
    7.10          val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
    7.11  
     8.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Jun 11 13:57:59 2016 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Jun 11 16:41:11 2016 +0200
     8.3 @@ -403,8 +403,8 @@
     8.4  val _ =
     8.5    Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
     8.6      "define primitive recursive functions on nominal datatypes"
     8.7 -    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_multi_specs
     8.8 -      >> (fn ((((invs, fctxt), fixes), params), specs) =>
     8.9 -        primrec_cmd invs fctxt fixes params specs));
    8.10 +    (options -- Parse.vars -- Parse.for_fixes -- Parse_Spec.where_multi_specs
    8.11 +      >> (fn ((((invs, fctxt), vars), params), specs) =>
    8.12 +        primrec_cmd invs fctxt vars params specs));
    8.13  
    8.14  end;
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Jun 11 13:57:59 2016 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Jun 11 16:41:11 2016 +0200
     9.3 @@ -2394,13 +2394,13 @@
     9.4  val _ = Outer_Syntax.local_theory @{command_keyword corec}
     9.5    "define nonprimitive corecursive functions"
     9.6    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
     9.7 -      --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop)
     9.8 +      --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
     9.9     >> uncurry corec_cmd);
    9.10  
    9.11  val _ = Outer_Syntax.local_theory_to_proof @{command_keyword corecursive}
    9.12    "define nonprimitive corecursive functions"
    9.13    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
    9.14 -      --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop)
    9.15 +      --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
    9.16     >> uncurry corecursive_cmd);
    9.17  
    9.18  val _ = Outer_Syntax.local_theory_to_proof @{command_keyword friend_of_corec}
    10.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Jun 11 13:57:59 2016 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Jun 11 16:41:11 2016 +0200
    10.3 @@ -1615,13 +1615,13 @@
    10.4    "define primitive corecursive functions"
    10.5    ((Scan.optional (@{keyword "("} |--
    10.6        Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
    10.7 -    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
    10.8 +    (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
    10.9  
   10.10  val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
   10.11    "define primitive corecursive functions"
   10.12    ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
   10.13        --| @{keyword ")"}) []) --
   10.14 -    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
   10.15 +    (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
   10.16  
   10.17  val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin
   10.18    gfp_rec_sugar_transfer_interpretation);
    11.1 --- a/src/HOL/Tools/Function/partial_function.ML	Sat Jun 11 13:57:59 2016 +0200
    11.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Sat Jun 11 16:41:11 2016 +0200
    11.3 @@ -313,7 +313,7 @@
    11.4  
    11.5  val _ =
    11.6    Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
    11.7 -    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.simple_spec)))
    11.8 -      >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
    11.9 +    ((mode -- (Parse.vars -- (Parse.where_ |-- Parse_Spec.simple_spec)))
   11.10 +      >> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec));
   11.11  
   11.12  end;
    12.1 --- a/src/HOL/Tools/inductive.ML	Sat Jun 11 13:57:59 2016 +0200
    12.2 +++ b/src/HOL/Tools/inductive.ML	Sat Jun 11 16:41:11 2016 +0200
    12.3 @@ -1169,7 +1169,7 @@
    12.4  (** outer syntax **)
    12.5  
    12.6  fun gen_ind_decl mk_def coind =
    12.7 -  Parse.fixes -- Parse.for_fixes --
    12.8 +  Parse.vars -- Parse.for_fixes --
    12.9    Scan.optional Parse_Spec.where_multi_specs [] --
   12.10    Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
   12.11    >> (fn (((preds, params), specs), monos) =>
    13.1 --- a/src/Pure/Isar/parse.ML	Sat Jun 11 13:57:59 2016 +0200
    13.2 +++ b/src/Pure/Isar/parse.ML	Sat Jun 11 16:41:11 2016 +0200
    13.3 @@ -88,7 +88,7 @@
    13.4    val const_decl: (string * string * mixfix) parser
    13.5    val const_binding: (binding * string * mixfix) parser
    13.6    val params: (binding * string option * mixfix) list parser
    13.7 -  val fixes: (binding * string option * mixfix) list parser
    13.8 +  val vars: (binding * string option * mixfix) list parser
    13.9    val for_fixes: (binding * string option * mixfix) list parser
   13.10    val ML_source: Input.source parser
   13.11    val document_source: Input.source parser
   13.12 @@ -374,8 +374,9 @@
   13.13      >> (fn ((x, ys), T) =>
   13.14          (x, Option.map #1 T, NoSyn) :: map (fn y => (y, Option.map #2 T, NoSyn)) ys);
   13.15  
   13.16 -val fixes = and_list1 (param_mixfix || params) >> flat;
   13.17 -val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
   13.18 +val vars = and_list1 (param_mixfix || params) >> flat;
   13.19 +
   13.20 +val for_fixes = Scan.optional ($$$ "for" |-- !!! vars) [];
   13.21  
   13.22  
   13.23  (* embedded source text *)
    14.1 --- a/src/Pure/Isar/parse_spec.ML	Sat Jun 11 13:57:59 2016 +0200
    14.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat Jun 11 16:41:11 2016 +0200
    14.3 @@ -67,7 +67,7 @@
    14.4  
    14.5  val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
    14.6  
    14.7 -val specification = Parse.fixes -- where_multi_specs;
    14.8 +val specification = Parse.vars -- where_multi_specs;
    14.9  
   14.10  
   14.11  (* basic constant specifications *)
   14.12 @@ -157,7 +157,7 @@
   14.13  
   14.14  val obtain_case =
   14.15    Parse.parbinding --
   14.16 -    (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
   14.17 +    (Scan.optional (Parse.and_list1 Parse.vars --| Parse.where_ >> flat) [] --
   14.18        (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
   14.19  
   14.20  val obtains = Parse.enum1 "|" obtain_case;
    15.1 --- a/src/Pure/Pure.thy	Sat Jun 11 13:57:59 2016 +0200
    15.2 +++ b/src/Pure/Pure.thy	Sat Jun 11 16:41:11 2016 +0200
    15.3 @@ -359,7 +359,7 @@
    15.4  
    15.5  val _ =
    15.6    Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
    15.7 -    (Scan.optional Parse.fixes [] --
    15.8 +    (Scan.optional Parse.vars [] --
    15.9        Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
   15.10        >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
   15.11  
   15.12 @@ -756,7 +756,7 @@
   15.13  
   15.14  val _ =
   15.15    Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
   15.16 -    (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
   15.17 +    (Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
   15.18  
   15.19  val _ =
   15.20    Outer_Syntax.command @{command_keyword assume} "assume propositions"
   15.21 @@ -768,7 +768,7 @@
   15.22  
   15.23  val _ =
   15.24    Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
   15.25 -    ((Parse.fixes --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
   15.26 +    ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
   15.27        >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
   15.28  
   15.29  val _ =
   15.30 @@ -786,12 +786,12 @@
   15.31  
   15.32  val _ =
   15.33    Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
   15.34 -    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
   15.35 +    (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
   15.36        >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
   15.37  
   15.38  val _ =
   15.39    Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
   15.40 -    (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
   15.41 +    (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
   15.42  
   15.43  val _ =
   15.44    Outer_Syntax.command @{command_keyword let} "bind text variables"