1.1 --- a/src/Pure/Isar/code.ML	Wed Nov 27 15:34:07 2013 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Nov 28 08:34:52 2013 +0100
     1.3 @@ -356,7 +356,7 @@
     1.4  fun analyze_constructor thy (c, ty) =
     1.5    let
     1.6      val _ = Thm.cterm_of thy (Const (c, ty));
     1.7 -    val ty_decl = Logic.unvarifyT_global (const_typ thy c);
     1.8 +    val ty_decl = devarify (const_typ thy c);
     1.9      fun last_typ c_ty ty =
    1.10        let
    1.11          val tfrees = Term.add_tfreesT ty [];
    1.12 @@ -664,7 +664,7 @@
    1.13        handle TERM _ => bad_thm "Not an abstype certificate";
    1.14      val _ = if param = rhs then () else bad_thm "Not an abstype certificate";
    1.15      val ((tyco, sorts), (abs, (vs, ty'))) =
    1.16 -      analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
    1.17 +      analyze_constructor thy (abs, devarify raw_ty);
    1.18      val ty = domain_type ty';
    1.19      val (vs', _) = typscheme thy (abs, ty');
    1.20    in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
    1.21 @@ -729,7 +729,7 @@
    1.22  
    1.23  fun empty_cert thy c = 
    1.24    let
    1.25 -    val raw_ty = Logic.unvarifyT_global (const_typ thy c);
    1.26 +    val raw_ty = devarify (const_typ thy c);
    1.27      val (vs, _) = typscheme thy (c, raw_ty);
    1.28      val sortargs = case Axclass.class_of_param thy c
    1.29       of SOME class => [[class]]
    1.30 @@ -1124,7 +1124,7 @@
    1.31      val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
    1.32      val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
    1.33      val (ws, vs) = chop pos zs;
    1.34 -    val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
    1.35 +    val T = devarify (Sign.the_const_type thy case_const);
    1.36      val Ts = binder_types T;
    1.37      val T_cong = nth Ts pos;
    1.38      fun mk_prem z = Free (z, T_cong);