# HG changeset patch
# User wenzelm
# Date 1236085663 -3600
# Node ID 556d1810cdad159c78c26276f1606a577287b452
# Parent  225fa48756b254c731741d1e27ec6abcea4282db
Thm.binding;

diff -r 225fa48756b2 -r 556d1810cdad src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -16,7 +16,7 @@
     -> (Attrib.binding * term) list -> local_theory -> local_theory
 
   val add_fixpat: Attrib.binding * string list -> theory -> theory
-  val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
+  val add_fixpat_i: Thm.binding * term list -> theory -> theory
   val add_matchers: (string * string) list -> theory -> theory
   val setup: theory -> theory
 end;
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -118,8 +118,7 @@
 fun attribute thy = attribute_i thy o intern_src thy;
 
 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
-    [((Binding.empty, []),
-      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+    [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
   |> fst |> maps snd;
 
 
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/class.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -265,8 +265,7 @@
     |> add_consts bname class base_sort sups supparams global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
-          [((Binding.empty, []),
-            Option.map (globalize param_map) raw_pred |> the_list)]
+          [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
     #> snd
     #> `get_axiom
     #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -9,11 +9,9 @@
 signature CONSTDEFS =
 sig
   val add_constdefs: (binding * string option) list *
-    ((binding * string option * mixfix) option *
-      (Attrib.binding * string)) list -> theory -> theory
+    ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory
   val add_constdefs_i: (binding * typ option) list *
-    ((binding * typ option * mixfix) option *
-      ((binding * attribute list) * term)) list -> theory -> theory
+    ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory
 end;
 
 structure Constdefs: CONSTDEFS =
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/element.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -296,7 +296,7 @@
   gen_witness_proof (fn after_qed' => fn propss =>
     Proof.map_context (K goal_ctxt)
     #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
-      cmd NONE after_qed' (map (pair (Binding.empty, [])) propss))
+      cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
     (fn wits => fn _ => after_qed wits) wit_propss [];
 
 end;
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -11,8 +11,8 @@
   val mk_def: Proof.context -> (string * term) list -> term list
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
-  val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
-    Proof.context -> (term * (string * thm)) list * Proof.context
+  val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
+    (term * (string * thm)) list * Proof.context
   val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     (term * term) * Proof.context
@@ -104,7 +104,7 @@
   end;
 
 fun add_def (var, rhs) ctxt =
-  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Binding.empty, []), rhs))] ctxt
+  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (Thm.empty_binding, rhs))] ctxt
   in ((lhs, th), ctxt') end;
 
 
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -40,11 +40,9 @@
 sig
   val thatN: string
   val obtain: string -> (binding * string option * mixfix) list ->
-    (Attrib.binding * (string * string list) list) list ->
-    bool -> Proof.state -> Proof.state
+    (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val obtain_i: string -> (binding * typ option * mixfix) list ->
-    ((binding * attribute list) * (term * term list) list) list ->
-    bool -> Proof.state -> Proof.state
+    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     (cterm list * thm list) * Proof.context
   val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
@@ -155,14 +153,14 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
+    |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume_i
       [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show_i NONE after_qed [((Binding.empty, []), [(thesis, [])])] false
+    ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
@@ -295,7 +293,7 @@
         |> Proof.map_context (K ctxt')
         |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
-          (obtain_export fix_ctxt rule (map cert ts)) [((Binding.empty, []), asms)])
+          (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
         |> Proof.add_binds_i AutoBind.no_facts
       end;
 
@@ -313,7 +311,7 @@
     |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (apsnd (rpair I))
-      "guess" before_qed after_qed [((Binding.empty, []), [Logic.mk_term goal, goal])]
+      "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
     |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   end;
 
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -48,23 +48,18 @@
   val assm: Assumption.export ->
     (Attrib.binding * (string * string list) list) list -> state -> state
   val assm_i: Assumption.export ->
-    ((binding * attribute list) * (term * term list) list) list -> state -> state
+    (Thm.binding * (term * term list) list) list -> state -> state
   val assume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val assume_i: ((binding * attribute list) * (term * term list) list) list ->
-    state -> state
+  val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
   val presume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val presume_i: ((binding * attribute list) * (term * term list) list) list ->
-    state -> state
-  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
-    state -> state
-  val def_i: ((binding * attribute list) *
-    ((binding * mixfix) * (term * term list))) list -> state -> state
+  val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
+  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
+  val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
-  val note_thmss_i: ((binding * attribute list) *
-    (thm list * attribute list) list) list -> state -> state
+  val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
   val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
@@ -107,11 +102,11 @@
   val have: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state) ->
-    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state) ->
-    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) Future.future) ->
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -103,12 +103,10 @@
   val sticky_prefix: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
-  val note_thmss: string ->
-    ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
-      Proof.context -> (string * thm list) list * Proof.context
-  val note_thmss_i: string ->
-    ((binding * attribute list) * (thm list * attribute list) list) list ->
-      Proof.context -> (string * thm list) list * Proof.context
+  val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
+  val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   val read_vars: (binding * string option * mixfix) list -> Proof.context ->
     (binding * typ option * mixfix) list * Proof.context
@@ -121,10 +119,10 @@
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
-    ((binding * attribute list) * (string * string list) list) list ->
+    (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_assms_i: Assumption.export ->
-    ((binding * attribute list) * (term * term list) list) list ->
+    (Thm.binding * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
   val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/axclass.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -8,7 +8,7 @@
 signature AX_CLASS =
 sig
   val define_class: bstring * class list -> string list ->
-    ((binding * attribute list) * term list) list -> theory -> class * theory
+    (Thm.binding * term list) list -> theory -> class * theory
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
diff -r 225fa48756b2 -r 556d1810cdad src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -31,10 +31,10 @@
   val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
-  val note_thmss: string -> ((binding * attribute list) *
-    (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
-  val note_thmss_grouped: string -> string -> ((binding * attribute list) *
-    (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+  val note_thmss: string -> (Thm.binding *
+      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+  val note_thmss_grouped: string -> string -> (Thm.binding *
+      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
   val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->
@@ -151,14 +151,15 @@
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b
   then swap (enter_proofs (app_att (thy, thms)))
-  else let
-    val naming = Sign.naming_of thy;
-    val name = NameSpace.full_name naming b;
-    val (thy', thms') =
-      enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
-    val thms'' = map (Thm.transfer thy') thms';
-    val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
-  in (thms'', thy'') end;
+  else
+    let
+      val naming = Sign.naming_of thy;
+      val name = NameSpace.full_name naming b;
+      val (thy', thms') =
+        enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+      val thms'' = map (Thm.transfer thy') thms';
+      val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
+    in (thms'', thy'') end;
 
 
 (* store_thm(s) *)
diff -r 225fa48756b2 -r 556d1810cdad src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Mar 03 14:07:23 2009 +0100
+++ b/src/Tools/induct.ML	Tue Mar 03 14:07:43 2009 +0100
@@ -552,7 +552,7 @@
   let
     fun add (SOME (SOME x, t)) ctxt =
           let val ([(lhs, (_, th))], ctxt') =
-            LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt
+            LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
           in ((SOME lhs, [th]), ctxt') end
       | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
       | add NONE ctxt = ((NONE, []), ctxt);