1.1 --- a/src/Pure/Isar/proof.ML Wed Dec 03 21:00:39 2008 -0800
1.2 +++ b/src/Pure/Isar/proof.ML Thu Dec 04 14:43:33 2008 +0100
1.3 @@ -45,27 +45,27 @@
1.4 val match_bind_i: (term list * term) list -> state -> state
1.5 val let_bind: (string list * string) list -> state -> state
1.6 val let_bind_i: (term list * term) list -> state -> state
1.7 - val fix: (Name.binding * string option * mixfix) list -> state -> state
1.8 - val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
1.9 + val fix: (Binding.T * string option * mixfix) list -> state -> state
1.10 + val fix_i: (Binding.T * typ option * mixfix) list -> state -> state
1.11 val assm: Assumption.export ->
1.12 (Attrib.binding * (string * string list) list) list -> state -> state
1.13 val assm_i: Assumption.export ->
1.14 - ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
1.15 + ((Binding.T * attribute list) * (term * term list) list) list -> state -> state
1.16 val assume: (Attrib.binding * (string * string list) list) list -> state -> state
1.17 - val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
1.18 + val assume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
1.19 state -> state
1.20 val presume: (Attrib.binding * (string * string list) list) list -> state -> state
1.21 - val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
1.22 + val presume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
1.23 state -> state
1.24 - val def: (Attrib.binding * ((Name.binding * mixfix) * (string * string list))) list ->
1.25 + val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list ->
1.26 state -> state
1.27 - val def_i: ((Name.binding * attribute list) *
1.28 - ((Name.binding * mixfix) * (term * term list))) list -> state -> state
1.29 + val def_i: ((Binding.T * attribute list) *
1.30 + ((Binding.T * mixfix) * (term * term list))) list -> state -> state
1.31 val chain: state -> state
1.32 val chain_facts: thm list -> state -> state
1.33 val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
1.34 val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
1.35 - val note_thmss_i: ((Name.binding * attribute list) *
1.36 + val note_thmss_i: ((Binding.T * attribute list) *
1.37 (thm list * attribute list) list) list -> state -> state
1.38 val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
1.39 val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
1.40 @@ -89,7 +89,7 @@
1.41 (theory -> 'a -> attribute) ->
1.42 (context * 'b list -> context * (term list list * (context -> context))) ->
1.43 string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
1.44 - ((Name.binding * 'a list) * 'b) list -> state -> state
1.45 + ((Binding.T * 'a list) * 'b) list -> state -> state
1.46 val local_qed: Method.text option * bool -> state -> state Seq.seq
1.47 val theorem: Method.text option -> (thm list list -> context -> context) ->
1.48 (string * string list) list list -> context -> state
1.49 @@ -109,11 +109,11 @@
1.50 val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
1.51 (Attrib.binding * (string * string list) list) list -> bool -> state -> state
1.52 val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
1.53 - ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
1.54 + ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
1.55 val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
1.56 (Attrib.binding * (string * string list) list) list -> bool -> state -> state
1.57 val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
1.58 - ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
1.59 + ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
1.60 val is_relevant: state -> bool
1.61 val future_proof: (state -> context) -> state -> context
1.62 end;
1.63 @@ -617,7 +617,7 @@
1.64
1.65 (* note etc. *)
1.66
1.67 -fun no_binding args = map (pair (Name.no_binding, [])) args;
1.68 +fun no_binding args = map (pair (Binding.empty, [])) args;
1.69
1.70 local
1.71
1.72 @@ -645,7 +645,7 @@
1.73 val local_results =
1.74 gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
1.75
1.76 -fun get_thmss state srcs = the_facts (note_thmss [((Name.no_binding, []), srcs)] state);
1.77 +fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
1.78
1.79 end;
1.80
1.81 @@ -689,14 +689,14 @@
1.82 val atts = map (prep_att (theory_of state)) raw_atts;
1.83 val (asms, state') = state |> map_context_result (fn ctxt =>
1.84 ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
1.85 - val assumptions = asms |> map (fn (a, ts) => ((Name.binding a, atts), map (rpair []) ts));
1.86 + val assumptions = asms |> map (fn (a, ts) => ((Binding.name a, atts), map (rpair []) ts));
1.87 in
1.88 state'
1.89 |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
1.90 |> assume_i assumptions
1.91 |> add_binds_i AutoBind.no_facts
1.92 |> map_context (ProofContext.restore_naming (context_of state))
1.93 - |> `the_facts |-> (fn thms => note_thmss_i [((Name.binding name, []), [(thms, [])])])
1.94 + |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
1.95 end;
1.96
1.97 in
1.98 @@ -1002,7 +1002,7 @@
1.99 val statement' = (kind, [[], [Thm.term_of cprop_protected]], cprop_protected);
1.100 val goal' = Thm.adjust_maxidx_thm ~1 (Drule.protectI RS Goal.init cprop_protected);
1.101 fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
1.102 - val this_name = ProofContext.full_name (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
1.103 + val this_name = ProofContext.full_bname (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
1.104
1.105 fun make_result () = state
1.106 |> map_contexts (Variable.auto_fixes prop)