# HG changeset patch
# User haftmann
# Date 1293092443 -3600
# Node ID cf5ab80b6717bef465051ce85c40cf6202174c04
# Parent  51c866d1b53b3d9ff54e590ea32b0ef490f9f41c
tuned comments and line breaks

diff -r 51c866d1b53b -r cf5ab80b6717 src/HOL/Tools/type_lifting.ML
--- a/src/HOL/Tools/type_lifting.ML	Wed Dec 22 18:24:04 2010 -0800
+++ b/src/HOL/Tools/type_lifting.ML	Thu Dec 23 09:20:43 2010 +0100
@@ -17,15 +17,13 @@
 structure Type_Lifting : TYPE_LIFTING =
 struct
 
+(* bookkeeping *)
+
 val compN = "comp";
 val idN = "id";
 val compositionalityN = "compositionality";
 val identityN = "identity";
 
-(** functorial mappers and their properties **)
-
-(* bookkeeping *)
-
 type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   comp: thm, id: thm };
 
@@ -114,13 +112,16 @@
       else
         HOLogic.mk_comp (Free (f32, T32), Free (f21, T21))
       ) contras (args21 ~~ args32)
-    fun mk_mapper T T' args = list_comb (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
+    fun mk_mapper T T' args = list_comb
+      (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args);
     val mapper21 = mk_mapper T2 T1 (map Free args21);
     val mapper32 = mk_mapper T3 T2 (map Free args32);
     val mapper31 = mk_mapper T3 T1 args31;
-    val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (HOLogic.mk_comp (mapper21, mapper32), mapper31);
+    val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+      (HOLogic.mk_comp (mapper21, mapper32), mapper31);
     val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3)
-    val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (mapper21 $ (mapper32 $ x), mapper31 $ x);
+    val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+      (mapper21 $ (mapper32 $ x), mapper31 $ x);
     val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
     val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
     fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop
@@ -144,7 +145,8 @@
     val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
     val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
     val rhs = HOLogic.id_const T;
-    val (id_prop, identity_prop) = pairself (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
+    val (id_prop, identity_prop) = pairself
+      (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
     fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop
       (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss)));
   in (id_prop, prove_identity) end;