# HG changeset patch
# User wenzelm
# Date 1137111191 -3600
# Node ID c3f445b92afff76ec17e84a85133ed035b9b4a73
# Parent  cd6d6baf041103ebff85e54298d7c6626a68b35d
uniform handling of fixes;

diff -r cd6d6baf0411 -r c3f445b92aff src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jan 13 01:13:08 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 13 01:13:11 2006 +0100
@@ -177,15 +177,13 @@
 
 (* constant definitions *)
 
-val vars = P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ));
-
 val structs =
-  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (vars --| P.$$$ ")")) [];
+  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
 
 val constdecl =
-  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, Syntax.NoSyn)) ||
+  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, NoSyn)) ||
     P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix' >> P.triple1 ||
-    P.name -- (P.mixfix' >> pair NONE) >> P.triple2;
+    P.name -- (P.mixfix >> pair NONE) >> P.triple2;
 val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
 
 val constdefsP =
@@ -197,7 +195,7 @@
 
 val axiomatizationP =
   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
-    (P.and_list1 P.param -- Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) []
+    (P.fixes -- Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) []
     >> (Toplevel.theory o (#2 oo Specification.axiomatize)));
 
 
@@ -254,7 +252,7 @@
 
 val setupP =
   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
-    (P.text >> (Toplevel.theory o PureThy.generic_setup));
+    (Scan.option P.text >> (Toplevel.theory o PureThy.generic_setup));
 
 val method_setupP =
   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
@@ -316,7 +314,8 @@
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
     ((P.opt_keyword "open" >> not) -- P.name
         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
-      >> (Toplevel.theory_context o (fn ((x, y), (z, w)) => Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt)))));
+      >> (Toplevel.theory_context o (fn ((x, y), (z, w)) =>
+          Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt)))));
 
 val opt_inst =
   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
@@ -418,7 +417,7 @@
 val fixP =
   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
     (K.tag_proof K.prf_asm)
-    (vars >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
+    (P.simple_fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
 
 val assumeP =
   OuterSyntax.command "assume" "assume propositions"
@@ -440,16 +439,13 @@
 val obtainP =
   OuterSyntax.command "obtain" "generalized existence"
     (K.tag_proof K.prf_asm_goal)
-    (Scan.optional
-      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
-        --| P.$$$ "where") [] -- statement
+    (Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- statement
       >> (Toplevel.print oo (Toplevel.proof' o uncurry Obtain.obtain)));
 
 val guessP =
   OuterSyntax.command "guess" "wild guessing (unstructured)"
     (K.tag_proof K.prf_asm_goal)
-    (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
-      >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
+    (Scan.optional P.simple_fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
 
 val letP =
   OuterSyntax.command "let" "bind text variables"
@@ -651,13 +647,14 @@
 
 val print_localeP =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
-    (Scan.optional (P.$$$ "!" >> K true) false -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
+    (Scan.optional (P.$$$ "!" >> K true) false -- locale_val
+      >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val print_registrationsP =
   OuterSyntax.improper_command "print_interps"
     "print interpretations of named locale" K.diag
-    (Scan.optional (P.$$$ "!" >> K true) false -- P.xname >>
-      (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
+    (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
+      >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
 
 val print_attributesP =
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
diff -r cd6d6baf0411 -r c3f445b92aff src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Jan 13 01:13:08 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Fri Jan 13 01:13:11 2006 +0100
@@ -36,22 +36,23 @@
 
 signature OBTAIN =
 sig
-  val obtain: (string list * string option) list ->
+  val obtain: (string * string option) list ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list
     -> bool -> Proof.state -> Proof.state
-  val obtain_i: (string list * typ option) list ->
+  val obtain_i: (string * typ option) list ->
     ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
     -> bool -> Proof.state -> Proof.state
-  val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state
-  val guess_i: (string list * typ option) 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
 end;
 
 structure Obtain: OBTAIN =
 struct
 
-(** export_obtained **)
 
-fun export_obtained state parms rule cprops thm =
+(** obtain_export **)
+
+fun obtain_export state parms rule cprops thm =
   let
     val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
     val cparms = map (Thm.cterm_of thy) parms;
@@ -78,9 +79,9 @@
 (** obtain **)
 
 fun bind_judgment ctxt name =
-  let val (t as _ $ Free v) =
-    ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name
-    |> ProofContext.bind_skolem ctxt [name]
+  let
+    val (bind, _) = ProofContext.bind_fixes [name] ctxt;
+    val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
   in (v, t) end;
 
 local
@@ -94,9 +95,10 @@
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*obtain vars*)
-    val (vars, vars_ctxt) = fold_map prep_vars raw_vars ctxt;
-    val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
-    val xs = List.concat (map fst vars);
+    val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
+    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+    val xs = map #1 vars;
+    val Ts = map #2 vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -126,14 +128,14 @@
     fun after_qed _ =
       Proof.local_qed (NONE, false)
       #> Seq.map (`Proof.the_fact #-> (fn rule =>
-        Proof.fix_i vars
-        #> Proof.assm_i (K (export_obtained state parms rule)) asms));
+        Proof.fix_i (xs ~~ Ts)
+        #> Proof.assm_i (K (obtain_export state 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)]
     |> Proof.assume_i
       [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
     |> `Proof.the_facts
@@ -205,8 +207,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 varss = #1 (fold_map prep_vars raw_vars ctxt);
-    val vars = List.concat (map (fn (xs, T) => map (rpair T) xs) varss);
+    val (vars, _) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
 
     fun check_result th =
       (case Thm.prems_of th of
@@ -221,8 +222,9 @@
 
     fun guess_context raw_rule =
       let
-        val (parms, rule) = match_params state vars raw_rule;
-        val ts = map (ProofContext.bind_skolem ctxt (map #1 parms) o Free) parms;
+        val (parms, rule) = match_params state (map (fn (x, T, _) => (x, T)) vars) raw_rule;
+        val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
+        val ts = map (bind o Free) parms;
         val ps = map dest_Free ts;
         val asms =
           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
@@ -230,8 +232,8 @@
         val _ = conditional (null asms) (fn () =>
           raise Proof.STATE ("Trivial result -- nothing guessed", state));
       in
-        Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms)
-        #> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)]
+        Proof.fix_i (map (apsnd SOME) parms)
+        #> Proof.assm_i (K (obtain_export state ts rule)) [(("", []), asms)]
         #> Proof.add_binds_i AutoBind.no_facts
       end;
 
@@ -242,7 +244,7 @@
     state
     |> Proof.enter_forward
     |> Proof.begin_block
-    |> Proof.fix_i [([AutoBind.thesisN], NONE)]
+    |> Proof.fix_i [(AutoBind.thesisN, NONE)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
       "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
diff -r cd6d6baf0411 -r c3f445b92aff src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Jan 13 01:13:08 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Jan 13 01:13:11 2006 +0100
@@ -42,12 +42,12 @@
   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 list * string option) list -> state -> state
-  val fix_i: (string list * typ option) list -> state -> state
-  val assm: ProofContext.exporter ->
+  val fix: (string * string option) list -> state -> state
+  val fix_i: (string * typ option) list -> state -> state
+  val assm: ProofContext.export ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     state -> state
-  val assm_i: ProofContext.exporter ->
+  val assm_i: ProofContext.export ->
     ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
@@ -359,7 +359,7 @@
 
     val prt_ctxt =
       if ! verbose orelse mode = Forward then ProofContext.pretty_context context
-      else if mode = Backward then ProofContext.pretty_asms context
+      else if mode = Backward then ProofContext.pretty_ctxt context
       else [];
   in
     [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
@@ -515,15 +515,15 @@
 
 local
 
-fun gen_fix fix_ctxt args =
+fun gen_fix add_fixes args =
   assert_forward
-  #> map_context (fix_ctxt args)
+  #> map_context (snd o add_fixes (map Syntax.no_syn args))
   #> put_facts NONE;
 
 in
 
-val fix = gen_fix ProofContext.fix;
-val fix_i = gen_fix ProofContext.fix_i;
+val fix = gen_fix ProofContext.add_fixes;
+val fix_i = gen_fix ProofContext.add_fixes_i;
 
 end;
 
@@ -540,12 +540,12 @@
 
 in
 
-val assm      = gen_assume ProofContext.assume Attrib.local_attribute;
-val assm_i    = gen_assume ProofContext.assume_i (K I);
-val assume    = assm ProofContext.export_assume;
-val assume_i  = assm_i ProofContext.export_assume;
-val presume   = assm ProofContext.export_presume;
-val presume_i = assm_i ProofContext.export_presume;
+val assm      = gen_assume ProofContext.add_assms Attrib.local_attribute;
+val assm_i    = gen_assume ProofContext.add_assms_i (K I);
+val assume    = assm ProofContext.assume_export;
+val assume_i  = assm_i ProofContext.assume_export;
+val presume   = assm ProofContext.presume_export;
+val presume_i = assm_i ProofContext.presume_export;
 
 end;
 
@@ -566,8 +566,8 @@
     val eqs = ProofContext.mk_def (context_of state') (xs ~~ rhss);
   in
     state'
-    |> fix [(xs, NONE)]
-    |> assm_i ProofContext.export_def ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
+    |> fix (map (rpair NONE) xs)
+    |> assm_i ProofContext.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
   end;
 
 in
@@ -787,6 +787,7 @@
     goal_state
     |> tap (check_tvars props)
     |> tap (check_vars props)
+    |> 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))
     |> map_context (ProofContext.auto_bind_goal props)
@@ -868,7 +869,7 @@
       #> after_qed results;
   in
     init ctxt
-    |> generic_goal (prepp #> ProofContext.auto_fix) (kind ^ goal_names target name names)
+    |> generic_goal (prepp #> ProofContext.auto_fixes) (kind ^ goal_names target name names)
       before_qed (K Seq.single, after_qed') propp
   end;
 
diff -r cd6d6baf0411 -r c3f445b92aff src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Jan 13 01:13:08 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Jan 13 01:13:11 2006 +0100
@@ -43,31 +43,27 @@
 
 (* prepare specification *)
 
-fun prep_specification prep_typ prep_propp prep_att
-    (raw_params, raw_specs) context =
+fun prep_specification prep_vars prep_propp prep_att
+    (raw_vars, raw_specs) ctxt =
   let
-    fun prep_param (x, raw_T, mx) ctxt =
-      let
-        val x' = Syntax.const_name x mx and mx' = Syntax.fix_mixfix x mx;
-        val T = Option.map (prep_typ ctxt) raw_T;
-      in ((x', mx'), ProofContext.add_fixes [(x', T, SOME mx')] ctxt) end;
+    val thy = ProofContext.theory_of ctxt;
 
-    val ((xs, mxs), params_ctxt) =
-      context |> fold_map prep_param raw_params |>> split_list;
-    val ((specs, vars), specs_ctxt) =
+    val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
+    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+    val ((specs, vs), specs_ctxt) =
       prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs)
       |> swap |>> map (map fst)
-      ||>> fold_map ProofContext.declared_type xs;
+      ||>> fold_map ProofContext.inferred_type xs;
 
-    val params = map2 (fn (x, T) => fn mx => (x, T, mx)) vars mxs;
+    val params = map2 (fn (x, T) => fn (_, _, mx) => (x, T, mx)) vs vars;
     val names = map (fst o fst) raw_specs;
-    val atts = map (map (prep_att (ProofContext.theory_of context)) o snd o fst) raw_specs;
+    val atts = map (map (prep_att thy) o snd o fst) raw_specs;
   in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
 
 fun read_specification x =
-  prep_specification ProofContext.read_typ ProofContext.read_propp Attrib.generic_attribute x;
+  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.generic_attribute x;
 fun cert_specification x =
-  prep_specification ProofContext.cert_typ ProofContext.cert_propp (K I) x;
+  prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
 
 
 (* axiomatize *)
diff -r cd6d6baf0411 -r c3f445b92aff src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Jan 13 01:13:08 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Jan 13 01:13:11 2006 +0100
@@ -173,7 +173,7 @@
              | _ => NONE)
       |> Library.flat
       |> map (fn (c, ty, syn) =>
-           ((c, the ty), (Syntax.unlocalize_mixfix o Syntax.fix_mixfix c o the) syn))
+           ((c, the ty), (Syntax.unlocalize_mixfix o Syntax.fix_mixfix c) syn))
       |> `(fn consts => extract_tyvar_name thy (map (snd o fst) consts))
       |-> (fn v => map ((apfst o apsnd) (subst_clsvar v (TFree (v, []))))
          #> pair v);