# HG changeset patch
# User haftmann
# Date 1385624092 -3600
# Node ID 89d5b69e5a081ab9c79a29ffb82faaa19a6f524e
# Parent  16879025203875c82d7904bd3e0a02d9e790084b
prefer name-normalizing devarify over unvarifyT whenever appropriate

diff -r 168790252038 -r 89d5b69e5a08 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Nov 27 15:34:07 2013 +0100
+++ b/src/Pure/Isar/code.ML	Thu Nov 28 08:34:52 2013 +0100
@@ -356,7 +356,7 @@
 fun analyze_constructor thy (c, ty) =
   let
     val _ = Thm.cterm_of thy (Const (c, ty));
-    val ty_decl = Logic.unvarifyT_global (const_typ thy c);
+    val ty_decl = devarify (const_typ thy c);
     fun last_typ c_ty ty =
       let
         val tfrees = Term.add_tfreesT ty [];
@@ -664,7 +664,7 @@
       handle TERM _ => bad_thm "Not an abstype certificate";
     val _ = if param = rhs then () else bad_thm "Not an abstype certificate";
     val ((tyco, sorts), (abs, (vs, ty'))) =
-      analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
+      analyze_constructor thy (abs, devarify raw_ty);
     val ty = domain_type ty';
     val (vs', _) = typscheme thy (abs, ty');
   in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
@@ -729,7 +729,7 @@
 
 fun empty_cert thy c = 
   let
-    val raw_ty = Logic.unvarifyT_global (const_typ thy c);
+    val raw_ty = devarify (const_typ thy c);
     val (vs, _) = typscheme thy (c, raw_ty);
     val sortargs = case Axclass.class_of_param thy c
      of SOME class => [[class]]
@@ -1124,7 +1124,7 @@
     val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
     val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
     val (ws, vs) = chop pos zs;
-    val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
+    val T = devarify (Sign.the_const_type thy case_const);
     val Ts = binder_types T;
     val T_cong = nth Ts pos;
     fun mk_prem z = Free (z, T_cong);