--- a/src/Pure/Isar/generic_target.ML Sat Nov 05 21:36:56 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML Sat Nov 05 22:01:19 2011 +0100
@@ -106,14 +106,16 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
- val assms = map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
- (Assumption.all_assms_of ctxt);
+ val assms =
+ map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
+ (Assumption.all_assms_of ctxt);
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
(*export fixes*)
val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
val frees = map Free (Thm.fold_terms Term.add_frees th' []);
- val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
+ val (th'' :: vs) =
+ (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
|> Variable.export ctxt thy_ctxt
|> Drule.zero_var_indexes_list;
@@ -183,6 +185,7 @@
end;
+
(** primitive theory operations **)
fun theory_declaration decl lthy =