diff -r 5b4a8b1d0f88 -r 11f531354852 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Tue Jan 08 11:37:29 2008 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Tue Jan 08 11:37:30 2008 +0100
@@ -60,23 +60,23 @@
 
 fun prove_size_thms (info : datatype_info) new_type_names thy =
   let
-    val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info;
+    val {descr, alt_names, sorts = raw_sorts, rec_names, rec_rewrites, induction, ...} = info;
 
     (*normalize type variable names to accomodate policy imposed by instantiation target*)
-    val tvars = (map dest_TFree o snd o dest_Type o hd) (get_rec_types descr sorts)
-      ~~ Name.invents Name.context Name.aT (length sorts);
-    val norm_tvars = map_atyps
-      (fn TFree (v, sort) => TFree (the (AList.lookup (op =) tvars v), sort));
+    val tvars = (map dest_TFree o snd o dest_Type o hd) (get_rec_types descr raw_sorts)
+      ~~ Name.invents Name.context Name.aT (length raw_sorts);
+    val sorts = tvars
+      |> map (fn (v, _) => (v, the (AList.lookup (op =) raw_sorts v)));
 
     val l = length new_type_names;
     val alt_names' = (case alt_names of
       NONE => replicate l NONE | SOME names => map SOME names);
     val descr' = List.take (descr, l);
     val (rec_names1, rec_names2) = chop l rec_names;
-    val recTs = map norm_tvars (get_rec_types descr sorts);
+    val recTs = get_rec_types descr sorts;
     val (recTs1, recTs2) = chop l recTs;
     val (_, (_, paramdts, _)) :: _ = descr;
-    val paramTs = map (norm_tvars o typ_of_dtyp descr sorts) paramdts;
+    val paramTs = map (typ_of_dtyp descr sorts) paramdts;
     val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
       map (fn T as TFree (s, _) =>
         let
@@ -108,7 +108,7 @@
     (* instantiation for primrec combinator *)
     fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
       let
-        val Ts = map (norm_tvars o typ_of_dtyp descr sorts) cargs;
+        val Ts = map (typ_of_dtyp descr sorts) cargs;
         val k = length (filter is_rec_type cargs);
         val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
           if is_rec_type dt then (Bound i :: us, i + 1, j + 1)
@@ -139,18 +139,12 @@
     fun define_overloaded (def_name, eq) lthy =
       let
         val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
-        val (thm, lthy') = lthy
+        val ((_, (_, thm)), lthy') = lthy
           |> LocalTheory.define Thm.definitionK ((c, NoSyn), ((def_name, []), rhs));
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
-        val thm' = thm
-          |> Assumption.export false lthy' ctxt_thy o snd o snd
-          |> singleton (Variable.export lthy' ctxt_thy)
+        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
 
-    val size_sorts = tvars
-      |> map (fn (v, _) => Sorts.inter_sort (Sign.classes_of thy) (HOLogic.typeS,
-           the (AList.lookup (op =) sorts v)));
-
     val ((size_def_thms, size_def_thms'), thy') =
       thy
       |> Sign.add_consts_i (map (fn (s, T) =>
@@ -160,7 +154,7 @@
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (def_names ~~ (size_fns ~~ rec_combs1)))
       ||> TheoryTarget.instantiation
-           (map (#1 o snd) descr', size_sorts, [HOLogic.class_size])
+           (map (#1 o snd) descr', sorts, [HOLogic.class_size])
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
       ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
@@ -192,7 +186,7 @@
     (* characteristic equations for size functions *)
     fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
       let
-        val Ts = map (norm_tvars o typ_of_dtyp descr sorts) cargs;
+        val Ts = map (typ_of_dtyp descr sorts) cargs;
         val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts);
         val ts = List.mapPartial (fn (sT as (s, T), dt) =>
           Option.map (fn sz => sz $ Free sT)