# HG changeset patch
# User wenzelm
# Date 1320501649 -3600
# Node ID e209da839ff4d1005f6fc2d392286742203d381e
# Parent  873e9c0ca37d2d9a62030b6cb297842691ea5dc7
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
tuned;

diff -r 873e9c0ca37d -r e209da839ff4 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 05 10:59:11 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 05 15:00:49 2011 +0100
@@ -75,7 +75,7 @@
         (map mk_partial_term_of (frees ~~ tys))
         (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
     val insts =
-      map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+      map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
         [Free ("ty", Term.itselfT ty), narrowing_term, rhs]
     val cty = Thm.ctyp_of thy ty;
   in
@@ -93,9 +93,10 @@
     val cs = (map o apsnd o apsnd o map o map_atyps)
       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
     val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
-    val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+    val var_insts =
+      map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
         [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
-          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
+          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
     val var_eq =
       @{thm partial_term_of_anything}
       |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts
diff -r 873e9c0ca37d -r e209da839ff4 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Sat Nov 05 10:59:11 2011 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Sat Nov 05 15:00:49 2011 +0100
@@ -59,8 +59,10 @@
     val t = list_comb (Const (c, tys ---> ty),
       map Free (Name.invent_names Name.context "a" tys));
     val (arg, rhs) =
-      pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
-        (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+      pairself (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
+        (t,
+          map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
+            (HOLogic.reflect_term t));
     val cty = Thm.ctyp_of thy ty;
   in
     @{thm term_of_anything}
diff -r 873e9c0ca37d -r e209da839ff4 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Nov 05 10:59:11 2011 +0100
+++ b/src/Pure/Isar/class.ML	Sat Nov 05 15:00:49 2011 +0100
@@ -344,7 +344,7 @@
     val c' = Sign.full_name thy b;
     val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     val ty' = Term.fastype_of rhs';
-    val rhs'' = map_types Logic.varifyT_global rhs';
+    val rhs'' = Logic.varify_types_global rhs';
   in
     thy
     |> Sign.add_abbrev (#1 prmode) (b, rhs'')
diff -r 873e9c0ca37d -r e209da839ff4 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Nov 05 10:59:11 2011 +0100
+++ b/src/Pure/Isar/code.ML	Sat Nov 05 15:00:49 2011 +0100
@@ -131,12 +131,14 @@
   let
     val c' = AxClass.unoverload_const thy (c, ty);
     val ty_decl = Sign.the_const_type thy c';
-  in if Sign.typ_equiv thy
-      (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) then c'
-    else error ("Type\n" ^ string_of_typ thy ty
-      ^ "\nof constant " ^ quote c
-      ^ "\nis too specific compared to declared type\n"
-      ^ string_of_typ thy ty_decl)
+  in
+    if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty))
+    then c'
+    else
+      error ("Type\n" ^ string_of_typ thy ty ^
+        "\nof constant " ^ quote c ^
+        "\nis too specific compared to declared type\n" ^
+        string_of_typ thy ty_decl)
   end; 
 
 fun check_const thy = check_unoverload thy o check_bare_const thy;
@@ -403,16 +405,18 @@
   let
     val _ = Thm.cterm_of thy (Const (c, raw_ty));
     val ty = subst_signature thy c raw_ty;
-    val ty_decl = (Logic.unvarifyT_global o const_typ thy) c;
+    val ty_decl = Logic.unvarifyT_global (const_typ thy c);
     fun last_typ c_ty ty =
       let
         val tfrees = Term.add_tfreesT ty [];
         val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty))
           handle TYPE _ => no_constr thy "bad type" c_ty
         val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
-        val _ = if has_duplicates (eq_fst (op =)) vs
+        val _ =
+          if has_duplicates (eq_fst (op =)) vs
           then no_constr thy "duplicate type variables in datatype" c_ty else ();
-        val _ = if length tfrees <> length vs
+        val _ =
+          if length tfrees <> length vs
           then no_constr thy "type variables missing in datatype" c_ty else ();
       in (tyco, vs) end;
     val (tyco, _) = last_typ (c, ty) ty_decl;
@@ -692,7 +696,8 @@
     val _ = (fst o dest_Var) param
       handle TERM _ => bad "Not an abstype certificate";
     val _ = if param = rhs then () else bad "Not an abstype certificate";
-    val ((tyco, sorts), (abs, (vs, ty'))) = analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
+    val ((tyco, sorts), (abs, (vs, ty'))) =
+      analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
     val ty = domain_type ty';
     val (vs', _) = logical_typscheme thy (abs, ty');
   in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
@@ -849,7 +854,7 @@
       let
         val vs = fst (typscheme_abs thy abs_thm);
         val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
-      in (vs, add_rhss_of_eqn thy (map_types Logic.unvarifyT_global (Thm.prop_of concrete_thm)) []) end;
+      in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end;
 
 fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
       let
@@ -865,7 +870,7 @@
       let
         val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
         val tyscm = typscheme_projection thy t;
-        val t' = map_types Logic.varifyT_global t;
+        val t' = Logic.varify_types_global t;
         fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
       in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
   | equations_of_cert thy (Abstract (abs_thm, tyco)) =
@@ -882,7 +887,7 @@
       (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
          o snd o equations_of_cert thy) cert
   | pretty_cert thy (Projection (t, _)) =
-      [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
+      [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
   | pretty_cert thy (Abstract (abs_thm, _)) =
       [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
 
@@ -1255,8 +1260,8 @@
   in
     thy
     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
-    |> change_fun_spec false rep ((K o Proj)
-        (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
+    |> change_fun_spec false rep
+      (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
     |> Abstype_Interpretation.data (tyco, serial ())
   end;
 
diff -r 873e9c0ca37d -r e209da839ff4 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Nov 05 10:59:11 2011 +0100
+++ b/src/Pure/goal.ML	Sat Nov 05 15:00:49 2011 +0100
@@ -168,8 +168,7 @@
     val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
 
     val global_prop =
-      cert (Term.map_types Logic.varifyT_global
-        (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
+      cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
       |> Thm.weaken_sorts (Variable.sorts_of ctxt);
     val global_result = result |> Future.map
       (Drule.flexflex_unique #>
diff -r 873e9c0ca37d -r e209da839ff4 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Nov 05 10:59:11 2011 +0100
+++ b/src/Pure/logic.ML	Sat Nov 05 15:00:49 2011 +0100
@@ -73,6 +73,8 @@
   val assum_problems: int * term -> (term -> term) * term list * term
   val varifyT_global: typ -> typ
   val unvarifyT_global: typ -> typ
+  val varify_types_global: term -> term
+  val unvarify_types_global: term -> term
   val varify_global: term -> term
   val unvarify_global: term -> term
   val get_goal: term -> int -> term
@@ -524,13 +526,20 @@
 val varifyT_global = Same.commit varifyT_global_same;
 val unvarifyT_global = Same.commit unvarifyT_global_same;
 
+fun varify_types_global tm = tm
+  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
+  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
+
+fun unvarify_types_global tm = tm
+  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
+  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
+
 fun varify_global tm = tm
   |> Same.commit (Term_Subst.map_aterms_same
     (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | _ => raise Same.SAME))
-  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
-  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
+  |> varify_types_global;
 
 fun unvarify_global tm = tm
   |> Same.commit (Term_Subst.map_aterms_same
@@ -538,8 +547,7 @@
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | Free (x, _) => raise TERM (bad_fixed x, [tm])
       | _ => raise Same.SAME))
-  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
-  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
+  |> unvarify_types_global;
 
 
 (* goal states *)