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"

     2.1 --- a/src/Pure/Isar/obtain.ML	Sun Jun 11 21:59:23 2006 +0200
     2.2 +++ b/src/Pure/Isar/obtain.ML	Sun Jun 11 21:59:24 2006 +0200
     2.3 @@ -39,14 +39,14 @@
     2.4  
     2.5  signature OBTAIN =
     2.6  sig
     2.7 -  val obtain: string -> (string * string option) list ->
     2.8 +  val obtain: string -> (string * string option * mixfix) list ->
     2.9      ((string * Attrib.src list) * (string * string list) list) list
    2.10      -> bool -> Proof.state -> Proof.state
    2.11 -  val obtain_i: string -> (string * typ option) list ->
    2.12 +  val obtain_i: string -> (string * typ option * mixfix) list ->
    2.13      ((string * attribute list) * (term * term list) list) list
    2.14      -> bool -> Proof.state -> Proof.state
    2.15 -  val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
    2.16 -  val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
    2.17 +  val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    2.18 +  val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    2.19    val statement: (string * ((string * 'typ option) list * 'term list)) list ->
    2.20      (('typ, 'term, 'fact) Element.ctxt list *
    2.21        ((string * Attrib.src list) * ('term * 'term list) list) list) *
    2.22 @@ -112,7 +112,7 @@
    2.23      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    2.24  
    2.25      (*obtain vars*)
    2.26 -    val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
    2.27 +    val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
    2.28      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    2.29      val xs = map #1 vars;
    2.30  
    2.31 @@ -145,14 +145,14 @@
    2.32      fun after_qed _ =
    2.33        Proof.local_qed (NONE, false)
    2.34        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    2.35 -        Proof.fix_i (xs ~~ map #2 vars)
    2.36 +        Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
    2.37          #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
    2.38    in
    2.39      state
    2.40      |> Proof.enter_forward
    2.41      |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
    2.42      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    2.43 -    |> Proof.fix_i [(thesisN, NONE)]
    2.44 +    |> Proof.fix_i [(thesisN, NONE, NoSyn)]
    2.45      |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
    2.46      |> `Proof.the_facts
    2.47      ||> Proof.chain_facts chain_facts
    2.48 @@ -231,8 +231,7 @@
    2.49      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    2.50  
    2.51      val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
    2.52 -    val vars = ctxt |> prep_vars (map Syntax.no_syn raw_vars)
    2.53 -      |-> fold_map inferred_type |> polymorphic;
    2.54 +    val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic;
    2.55  
    2.56      fun check_result th =
    2.57        (case Thm.prems_of th of
    2.58 @@ -254,7 +253,7 @@
    2.59            |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
    2.60          val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
    2.61        in
    2.62 -        Proof.fix_i (map (apsnd SOME) parms)
    2.63 +        Proof.fix_i (map2 (fn (x, T) => fn (_, mx) => (x, SOME T, mx)) parms vars)
    2.64          #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
    2.65          #> Proof.add_binds_i AutoBind.no_facts
    2.66        end;
    2.67 @@ -270,7 +269,7 @@
    2.68      state
    2.69      |> Proof.enter_forward
    2.70      |> Proof.begin_block
    2.71 -    |> Proof.fix_i [(AutoBind.thesisN, NONE)]
    2.72 +    |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)]
    2.73      |> Proof.chain_facts chain_facts
    2.74      |> Proof.local_goal print_result (K I) (apsnd (rpair I))
    2.75        "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]