# HG changeset patch
# User wenzelm
# Date 1247696496 -7200
# Node ID 5589a5360ddc0e7206610de8763cd42915e14986
# Parent  f2a8dbceb6154dac5cda344b462b014fecb97c14
eliminated legacy_varify;

diff -r f2a8dbceb615 -r 5589a5360ddc src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Jul 15 23:50:40 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Jul 16 00:21:36 2009 +0200
@@ -180,7 +180,7 @@
     val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
     val r = Const (case_name, map fastype_of rs ---> T --> rT);
 
-    val y = Var (("y", 0), Logic.legacy_varifyT T);
+    val y = Var (("y", 0), Logic.varifyT T);
     val y' = Free ("y", T);
 
     val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
@@ -201,10 +201,10 @@
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
     val prf = forall_intr_prf (y, forall_intr_prf (P,
       List.foldr (fn ((p, r), prf) =>
-        forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
+        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
           prf))) (Proofterm.proof_combP (prf_of thm',
             map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
-    val r' = Logic.legacy_varify (Abs ("y", Logic.legacy_varifyT T,
+    val r' = Logic.varify (Abs ("y", T,
       list_abs (map dest_Free rs, list_comb (r,
         map Bound ((length rs - 1 downto 0) @ [length rs])))));