# HG changeset patch
# User wenzelm
# Date 1150055966 -7200
# Node ID 3a2d33a5a7b6bde69d74803e5a976770ec5a78ac
# Parent  b8985bf2ce8bc1c3de6b1d9db3961bff1e2b84e8
fixes: include mixfix syntax;
goal: improved handling of implicit vars;

diff -r b8985bf2ce8b -r 3a2d33a5a7b6 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jun 11 21:59:25 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Jun 11 21:59:26 2006 +0200
@@ -44,8 +44,8 @@
   val match_bind_i: (term list * term) list -> state -> state
   val let_bind: (string list * string) list -> state -> state
   val let_bind_i: (term list * term) list -> state -> state
-  val fix: (string * string option) list -> state -> state
-  val fix_i: (string * typ option) list -> state -> state
+  val fix: (string * string option * mixfix) list -> state -> state
+  val fix_i: (string * typ option * mixfix) list -> state -> state
   val assm: ProofContext.export ->
     ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   val assm_i: ProofContext.export ->
@@ -54,8 +54,10 @@
   val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
   val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
-  val def: ((string * Attrib.src list) * (string * (string * string list))) list -> state -> state
-  val def_i: ((string * attribute list) * (string * (term * term list))) list -> state -> state
+  val def: ((string * Attrib.src list) *
+    ((string * mixfix) * (string * string list))) list -> state -> state
+  val def_i: ((string * attribute list) *
+    ((string * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
@@ -517,7 +519,7 @@
 
 fun gen_fix add_fixes args =
   assert_forward
-  #> map_context (snd o add_fixes (map Syntax.no_syn args))
+  #> map_context (snd o add_fixes args)
   #> put_facts NONE;
 
 in
@@ -554,19 +556,21 @@
 
 local
 
-fun gen_def fix prep_att prep_binds args state =
+fun gen_def gen_fix prep_att prep_binds args state =
   let
     val _ = assert_forward state;
     val thy = theory_of state;
 
-    val ((raw_names, raw_atts), (xs, raw_rhss)) = args |> split_list |>> split_list ||> split_list;
+    val ((raw_names, raw_atts), (vars, raw_rhss)) =
+      args |> split_list |>> split_list ||> split_list;
+    val xs = map #1 vars;
     val names = map (fn ("", x) => Thm.def_name x | (name, _) => name) (raw_names ~~ xs);
     val atts = map (map (prep_att thy)) raw_atts;
     val (rhss, state') = state |> map_context_result (prep_binds false (map swap raw_rhss));
     val eqs = LocalDefs.mk_def (context_of state') (xs ~~ rhss);
   in
     state'
-    |> fix (map (rpair NONE) xs)
+    |> gen_fix (map (fn (x, mx) => (x, NONE, mx)) vars)
     |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, [])]) eqs)
   end;
 
@@ -762,15 +766,15 @@
 
 local
 
-fun warn_tvars [] _ = ()
-  | warn_tvars vs state =
-      warning ("Goal statement contains unbound schematic type variable(s): " ^
-        commas (map (ProofContext.string_of_typ (context_of state) o TVar) vs));
-
-fun warn_vars [] _ = ()
-  | warn_vars vs state =
-      warning ("Goal statement contains unbound schematic variable(s): " ^
-        commas (map (ProofContext.string_of_term (context_of state) o Var) vs));
+fun implicit_vars dest add props =
+  let
+    val (explicit_vars, props') = take_prefix (can dest) props |>> map dest;
+    val vars = rev (subtract (op =) explicit_vars (fold add props []));
+    val _ =
+      if null vars then ()
+      else warning ("Goal statement contains unbound schematic variable(s): " ^
+        commas_quote (map (Term.string_of_vname o fst) vars));
+  in (rev vars, props') end;
 
 fun refine_terms n =
   refine (Method.Basic (K (Method.RAW_METHOD
@@ -793,10 +797,9 @@
       |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
     val props = flat propss;
 
-    val dest_var = Term.dest_Var o Logic.dest_term;
-    val explicit_vars = map dest_var (#1 (take_prefix (can dest_var) props));
-    val vars = rev ((fold o Term.fold_aterms) (fn Var v =>
-      if member (op =) explicit_vars v then I else insert (op =) v | _ => I) props []);
+    val (_, props') =
+      implicit_vars (dest_TVar o Logic.dest_type o Logic.dest_term) Term.add_tvars props;
+    val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
 
     val propss' = map (Logic.mk_term o Var) vars :: propss;
     val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss'));
@@ -804,8 +807,6 @@
       fn results => map_context after_ctxt #> after_local results);
   in
     goal_state
-    |> tap (warn_tvars (fold Term.add_tvars props []))
-    |> tap (warn_vars vars)
     |> map_context (ProofContext.set_body true)
     |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
     |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))