--- 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) *)