src/HOL/Tools/datatype_realizer.ML
changeset 59582 0fbed69ff081
parent 59498 50b60f501b05
child 59617 b60e65ad13df
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
     1.5    let
     1.6      val ctxt = Proof_Context.init_global thy;
     1.7 -    val cert = cterm_of thy;
     1.8 +    val cert = Thm.cterm_of thy;
     1.9  
    1.10      val recTs = Old_Datatype_Aux.get_rec_types descr;
    1.11      val pnames =
    1.12 @@ -107,7 +107,7 @@
    1.13            make_pred i U T (mk_proj i is r) (Free (tname, T)))
    1.14              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
    1.15      val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
    1.16 -      (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
    1.17 +      (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
    1.18  
    1.19      val thm =
    1.20        Goal.prove_internal ctxt (map cert prems) (cert concl)
    1.21 @@ -144,7 +144,7 @@
    1.22                      (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    1.23                  end
    1.24              | _ => AbsP ("H", SOME p, prf)))
    1.25 -          (rec_fns ~~ prems_of thm)
    1.26 +          (rec_fns ~~ Thm.prems_of thm)
    1.27            (Proofterm.proof_combP
    1.28              (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
    1.29  
    1.30 @@ -160,7 +160,7 @@
    1.31  fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
    1.32    let
    1.33      val ctxt = Proof_Context.init_global thy;
    1.34 -    val cert = cterm_of thy;
    1.35 +    val cert = Thm.cterm_of thy;
    1.36      val rT = TFree ("'P", @{sort type});
    1.37      val rT' = TVar (("'P", 0), @{sort type});
    1.38  
    1.39 @@ -214,7 +214,7 @@
    1.40              (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
    1.41      val prf' =
    1.42        Extraction.abs_corr_shyps thy' exhaust []
    1.43 -        (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
    1.44 +        (map Var (Term.add_vars (Thm.prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
    1.45      val r' =
    1.46        Logic.varify_global (Abs ("y", T,
    1.47          (fold_rev (Term.abs o dest_Free) rs