--- 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);