src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

 
 (* creates the list of premises for every intro rule *)
 (* theory -> term -> (string list, term list list) *)
 
 fun dest_code_eqn eqn = let
-  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
+  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify_global (Thm.prop_of eqn))
   val (func, args) = strip_comb lhs
 in ((func, args), rhs) end;
 
 (* TODO: does not work with higher order functions yet *)
 fun mk_rewr_eq (func, pred) =

             (*
             val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
             *)
             
             val thy'' = Fun_Pred.map
-              (fold Item_Net.update (map (apfst Logic.varify)
+              (fold Item_Net.update (map (apfst Logic.varify_global)
                 (distinct (op =) funs ~~ (#preds ind_result)))) thy'
             (*val _ = print_specs thy'' specs*)
           in
             (specs, thy'')
           end

         SOME c => SOME (Const (c, pred_type T))
       | NONE => NONE)
     | lookup_pred _ = NONE
     *)
     fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
-    val intro_t = (Logic.unvarify o prop_of) intro
+    val intro_t = Logic.unvarify_global (prop_of intro)
     val (prems, concl) = Logic.strip_horn intro_t
     val frees = map fst (Term.add_frees intro_t [])
     fun rewrite prem names =
       let
         (*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*)