1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 11 14:06:35 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 11 14:30:34 2010 +0200
1.3 @@ -91,7 +91,7 @@
1.4 val (c, thy') =
1.5 Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
1.6 val cdef = cname ^ "_def"
1.7 - val (ax, thy'') =
1.8 + val ((_, ax), thy'') =
1.9 Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
1.10 val ax' = Drule.export_without_context ax
1.11 in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
2.1 --- a/src/HOL/Tools/typedef.ML Sun Apr 11 14:06:35 2010 +0200
2.2 +++ b/src/HOL/Tools/typedef.ML Sun Apr 11 14:30:34 2010 +0200
2.3 @@ -117,7 +117,7 @@
2.4
2.5 val typedef_deps = Term.add_consts A [];
2.6
2.7 - val (axiom, axiom_thy) = consts_thy
2.8 + val ((axiom_name, axiom), axiom_thy) = consts_thy
2.9 |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
2.10 ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
2.11 ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
3.1 --- a/src/Pure/Isar/class_target.ML Sun Apr 11 14:06:35 2010 +0200
3.2 +++ b/src/Pure/Isar/class_target.ML Sun Apr 11 14:30:34 2010 +0200
3.3 @@ -333,8 +333,8 @@
3.4 |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
3.5 |> snd
3.6 |> Thm.add_def false false (b_def, def_eq)
3.7 - |>> Thm.varifyT_global
3.8 - |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
3.9 + |>> apsnd Thm.varifyT_global
3.10 + |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
3.11 #> snd
3.12 #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
3.13 |> Sign.add_const_constraint (c', SOME ty')
4.1 --- a/src/Pure/Isar/overloading.ML Sun Apr 11 14:06:35 2010 +0200
4.2 +++ b/src/Pure/Isar/overloading.ML Sun Apr 11 14:30:34 2010 +0200
4.3 @@ -165,8 +165,9 @@
4.4
4.5 fun declare c_ty = pair (Const c_ty);
4.6
4.7 -fun define checked b (c, t) = Thm.add_def (not checked) true
4.8 - (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
4.9 +fun define checked b (c, t) =
4.10 + Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
4.11 + #>> snd;
4.12
4.13 fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
4.14 #> Local_Theory.target synchronize_syntax
5.1 --- a/src/Pure/Isar/specification.ML Sun Apr 11 14:06:35 2010 +0200
5.2 +++ b/src/Pure/Isar/specification.ML Sun Apr 11 14:30:34 2010 +0200
5.3 @@ -173,7 +173,7 @@
5.4 fold_map Thm.add_axiom
5.5 (map (apfst (fn a => Binding.map_name (K a) b))
5.6 (PureThy.name_multi (Name.of_binding b) (map subst props)))
5.7 - #>> (fn ths => ((b, atts), [(ths, [])])));
5.8 + #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
5.9
5.10 (*facts*)
5.11 val (facts, facts_lthy) = axioms_thy
6.1 --- a/src/Pure/Isar/theory_target.ML Sun Apr 11 14:06:35 2010 +0200
6.2 +++ b/src/Pure/Isar/theory_target.ML Sun Apr 11 14:30:34 2010 +0200
6.3 @@ -315,7 +315,7 @@
6.4 | NONE =>
6.5 if is_some (Class_Target.instantiation_param lthy b)
6.6 then AxClass.define_overloaded name' (head, rhs')
6.7 - else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')));
6.8 + else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd);
6.9 val def = Local_Defs.trans_terms lthy3
6.10 [(*c == global.c xs*) local_def,
6.11 (*global.c xs == rhs'*) global_def,
7.1 --- a/src/Pure/axclass.ML Sun Apr 11 14:06:35 2010 +0200
7.2 +++ b/src/Pure/axclass.ML Sun Apr 11 14:30:34 2010 +0200
7.3 @@ -306,11 +306,11 @@
7.4 |-> (fn const' as Const (c'', _) =>
7.5 Thm.add_def false true
7.6 (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
7.7 - #>> Thm.varifyT_global
7.8 - #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
7.9 - #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
7.10 - #> snd
7.11 - #> pair (Const (c, T))))
7.12 + #>> apsnd Thm.varifyT_global
7.13 + #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
7.14 + #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
7.15 + #> snd
7.16 + #> pair (Const (c, T))))
7.17 ||> Sign.restore_naming thy
7.18 end;
7.19
7.20 @@ -325,7 +325,7 @@
7.21 in
7.22 thy
7.23 |> Thm.add_def false false (b', prop)
7.24 - |>> (fn thm => Drule.transitive_thm OF [eq, thm])
7.25 + |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
7.26 end;
7.27
7.28
7.29 @@ -515,7 +515,7 @@
7.30
7.31 fun add_axiom (b, prop) =
7.32 Thm.add_axiom (b, prop) #->
7.33 - (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
7.34 + (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
7.35
7.36 fun axiomatize prep mk name add raw_args thy =
7.37 let
8.1 --- a/src/Pure/more_thm.ML Sun Apr 11 14:06:35 2010 +0200
8.2 +++ b/src/Pure/more_thm.ML Sun Apr 11 14:30:34 2010 +0200
8.3 @@ -62,8 +62,8 @@
8.4 val forall_intr_frees: thm -> thm
8.5 val unvarify_global: thm -> thm
8.6 val close_derivation: thm -> thm
8.7 - val add_axiom: binding * term -> theory -> thm * theory
8.8 - val add_def: bool -> bool -> binding * term -> theory -> thm * theory
8.9 + val add_axiom: binding * term -> theory -> (string * thm) * theory
8.10 + val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
8.11 type binding = binding * attribute list
8.12 val empty_binding: binding
8.13 val rule_attribute: (Context.generic -> thm -> thm) -> attribute
8.14 @@ -347,31 +347,36 @@
8.15 fun add_axiom (b, prop) thy =
8.16 let
8.17 val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
8.18 +
8.19 val _ = Sign.no_vars (Syntax.pp_global thy) prop;
8.20 val (strip, recover, prop') = stripped_sorts thy prop;
8.21 val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
8.22 val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
8.23 +
8.24 val thy' =
8.25 Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
8.26 - val axm' = Thm.axiom thy' (Sign.full_name thy' b');
8.27 + val axm_name = Sign.full_name thy' b';
8.28 + val axm' = Thm.axiom thy' axm_name;
8.29 val thm =
8.30 Thm.instantiate (recover, []) axm'
8.31 |> unvarify_global
8.32 |> fold elim_implies of_sorts;
8.33 - in (thm, thy') end;
8.34 + in ((axm_name, thm), thy') end;
8.35
8.36 fun add_def unchecked overloaded (b, prop) thy =
8.37 let
8.38 val _ = Sign.no_vars (Syntax.pp_global thy) prop;
8.39 val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
8.40 val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
8.41 +
8.42 val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
8.43 - val axm' = Thm.axiom thy' (Sign.full_name thy' b);
8.44 + val axm_name = Sign.full_name thy' b;
8.45 + val axm' = Thm.axiom thy' axm_name;
8.46 val thm =
8.47 Thm.instantiate (recover, []) axm'
8.48 |> unvarify_global
8.49 |> fold_rev Thm.implies_intr prems;
8.50 - in (thm, thy') end;
8.51 + in ((axm_name, thm), thy') end;
8.52
8.53
8.54
9.1 --- a/src/Pure/pure_thy.ML Sun Apr 11 14:06:35 2010 +0200
9.2 +++ b/src/Pure/pure_thy.ML Sun Apr 11 14:30:34 2010 +0200
9.3 @@ -210,7 +210,7 @@
9.4 fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
9.5 let
9.6 val prop = prep thy (b, raw_prop);
9.7 - val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
9.8 + val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
9.9 val thm = def
9.10 |> Thm.forall_intr_frees
9.11 |> Thm.forall_elim_vars 0