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