# HG changeset patch
# User wenzelm
# Date 1150055964 -7200
# Node ID 2c1fdc397ded78ac63833d0dbc24a94923d31cdb
# Parent  67cb97e856ff2a6cfe27c64d4bb7d6938ec91f1d
fixes: include mixfix syntax;

diff -r 67cb97e856ff -r 2c1fdc397ded src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Jun 11 21:59:23 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 11 21:59:24 2006 +0200
@@ -449,7 +449,7 @@
 val fixP =
   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
     (K.tag_proof K.prf_asm)
-    (P.simple_fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
+    (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
 
 val assumeP =
   OuterSyntax.command "assume" "assume propositions"
@@ -465,19 +465,20 @@
   OuterSyntax.command "def" "local definition"
     (K.tag_proof K.prf_asm)
     (P.and_list1
-      (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
+      (P.opt_thm_name ":" --
+        ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
     >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
 
 val obtainP =
   OuterSyntax.command "obtain" "generalized existence"
     (K.tag_proof K.prf_asm_goal)
-    (P.parname -- Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- P.statement
+    (P.parname -- Scan.optional (P.fixes --| P.$$$ "where") [] -- P.statement
       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
 
 val guessP =
   OuterSyntax.command "guess" "wild guessing (unstructured)"
     (K.tag_proof K.prf_asm_goal)
-    (Scan.optional P.simple_fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
+    (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
 
 val letP =
   OuterSyntax.command "let" "bind text variables"
diff -r 67cb97e856ff -r 2c1fdc397ded src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jun 11 21:59:23 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jun 11 21:59:24 2006 +0200
@@ -39,14 +39,14 @@
 
 signature OBTAIN =
 sig
-  val obtain: string -> (string * string option) list ->
+  val obtain: string -> (string * string option * mixfix) list ->
     ((string * Attrib.src list) * (string * string list) list) list
     -> bool -> Proof.state -> Proof.state
-  val obtain_i: string -> (string * typ option) list ->
+  val obtain_i: string -> (string * typ option * mixfix) list ->
     ((string * attribute list) * (term * term list) list) list
     -> bool -> Proof.state -> Proof.state
-  val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
-  val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
+  val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+  val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   val statement: (string * ((string * 'typ option) list * 'term list)) list ->
     (('typ, 'term, 'fact) Element.ctxt list *
       ((string * Attrib.src list) * ('term * 'term list) list) list) *
@@ -112,7 +112,7 @@
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*obtain vars*)
-    val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
+    val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
     val xs = map #1 vars;
 
@@ -145,14 +145,14 @@
     fun after_qed _ =
       Proof.local_qed (NONE, false)
       #> Seq.map (`Proof.the_fact #-> (fn rule =>
-        Proof.fix_i (xs ~~ map #2 vars)
+        Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
         #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
   in
     state
     |> Proof.enter_forward
     |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
-    |> Proof.fix_i [(thesisN, NONE)]
+    |> Proof.fix_i [(thesisN, NONE, NoSyn)]
     |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
@@ -231,8 +231,7 @@
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
-    val vars = ctxt |> prep_vars (map Syntax.no_syn raw_vars)
-      |-> fold_map inferred_type |> polymorphic;
+    val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic;
 
     fun check_result th =
       (case Thm.prems_of th of
@@ -254,7 +253,7 @@
           |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
         val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
       in
-        Proof.fix_i (map (apsnd SOME) parms)
+        Proof.fix_i (map2 (fn (x, T) => fn (_, mx) => (x, SOME T, mx)) parms vars)
         #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
         #> Proof.add_binds_i AutoBind.no_facts
       end;
@@ -270,7 +269,7 @@
     state
     |> Proof.enter_forward
     |> Proof.begin_block
-    |> Proof.fix_i [(AutoBind.thesisN, NONE)]
+    |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (apsnd (rpair I))
       "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]