src/HOL/Tools/datatype_realizer.ML
changeset 19806 f860b7a98445
parent 18929 d81435108688
child 20071 8f3e1ddb50e6
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Jun 07 02:01:27 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Jun 07 02:01:28 2006 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4       (foldr (fn ((f, p), prf) =>
     1.5          (case head_of (strip_abs_body f) of
     1.6             Free (s, T) =>
     1.7 -             let val T' = Type.varifyT T
     1.8 +             let val T' = Logic.varifyT T
     1.9               in Abst (s, SOME T', Proofterm.prf_abstract_over
    1.10                 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    1.11               end
    1.12 @@ -164,8 +164,7 @@
    1.13  
    1.14  fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) =
    1.15    let
    1.16 -    val sg = sign_of thy;
    1.17 -    val cert = cterm_of sg;
    1.18 +    val cert = cterm_of thy;
    1.19      val rT = TFree ("'P", HOLogic.typeS);
    1.20      val rT' = TVar (("'P", 0), HOLogic.typeS);
    1.21  
    1.22 @@ -187,7 +186,7 @@
    1.23      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
    1.24      val r = Const (case_name, map fastype_of rs ---> T --> rT);
    1.25  
    1.26 -    val y = Var (("y", 0), Type.varifyT T);
    1.27 +    val y = Var (("y", 0), Logic.legacy_varifyT T);
    1.28      val y' = Free ("y", T);
    1.29  
    1.30      val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
    1.31 @@ -208,10 +207,10 @@
    1.32      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.33      val prf = forall_intr_prf (y, forall_intr_prf (P,
    1.34        foldr (fn ((p, r), prf) =>
    1.35 -        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
    1.36 +        forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
    1.37            prf))) (Proofterm.proof_combP (prf_of thm',
    1.38              map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
    1.39 -    val r' = Logic.varify (Abs ("y", Type.varifyT T,
    1.40 +    val r' = Logic.legacy_varify (Abs ("y", Logic.legacy_varifyT T,
    1.41        list_abs (map dest_Free rs, list_comb (r,
    1.42          map Bound ((length rs - 1 downto 0) @ [length rs])))));
    1.43