# HG changeset patch
# User wenzelm
# Date 1325263230 -3600
# Node ID 4dba48d010d5d34dc3e56b980158e57b28bf6d3e
# Parent  20e5060ab75cfbe88f69daeae3734c449b76c438
tuned;

diff -r 20e5060ab75c -r 4dba48d010d5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Dec 30 16:43:46 2011 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 30 17:40:30 2011 +0100
@@ -1589,7 +1589,7 @@
       (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
 
     val split_meta_prop =  (* FIXME local P *)
-      let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
+      let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT) in
         Logic.mk_equals
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
       end;
@@ -1626,7 +1626,6 @@
         surject
       end);
 
-
     val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
       Skip_Proof.prove_global defs_thy [] [] split_meta_prop
         (fn _ =>
@@ -1751,16 +1750,16 @@
 fun add_code ext_tyco vs extT ext simps inject thy =
   let
     val eq =
-      (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+      HOLogic.mk_Trueprop (HOLogic.mk_eq
         (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
-         Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
+         Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
     fun tac eq_def =
       Class.intro_classes_tac []
       THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
       THEN ALLGOALS (rtac @{thm refl});
     fun mk_eq thy eq_def =
       Simplifier.rewrite_rule
-        [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
+        [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
     fun mk_eq_refl thy =
       @{thm equal_refl}
       |> Thm.instantiate
@@ -2007,7 +2006,8 @@
           |> Sign.restore_naming thy
           |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
           |> Typedecl.abbrev_global
-            (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
+            (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0
+          |> snd
           |> Sign.qualified_path false binding
           |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
             (sel_decls ~~ (field_syntax @ [NoSyn]))
@@ -2065,7 +2065,7 @@
     (*split*)
     val split_meta_prop =
       let
-        val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
+        val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> propT);
       in
         Logic.mk_equals
          (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))