src/HOL/Tools/inductive_realizer.ML
changeset 21646 c07b5b0e8492
parent 21395 f34ac19659ae
child 21858 05f57309170c
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4      val (Const (s, _), ts) = strip_comb S;
     1.5      val params = map dest_Var ts;
     1.6      val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
     1.7 -    fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
     1.8 +    fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr),
     1.9        map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    1.10          filter_out (equal Extraction.nullT) (map
    1.11            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    1.12 @@ -189,7 +189,7 @@
    1.13            in if conclT = Extraction.nullT
    1.14              then list_abs_free (map dest_Free xs, HOLogic.unit)
    1.15              else list_abs_free (map dest_Free xs, list_comb
    1.16 -              (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
    1.17 +              (Free ("r" ^ Sign.base_name (Thm.get_name intr),
    1.18                  map fastype_of (rev args) ---> conclT), rev args))
    1.19            end
    1.20  
    1.21 @@ -226,7 +226,7 @@
    1.22      let
    1.23        val r = foldr1 HOLogic.mk_prod rlzs;
    1.24        val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
    1.25 -      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
    1.26 +      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr);
    1.27        val r' = list_abs_free (List.mapPartial (fn intr =>
    1.28          Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
    1.29            if length concls = 1 then r $ x else r)
    1.30 @@ -271,7 +271,7 @@
    1.31            else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
    1.32              mk_prf (tl rs) prems prf));
    1.33  
    1.34 -  in (Thm.name_of_thm rule, (vs,
    1.35 +  in (Thm.get_name rule, (vs,
    1.36      if rt = Extraction.nullt then rt else
    1.37        foldr (uncurry lambda) rt vs1,
    1.38      foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
    1.39 @@ -349,11 +349,11 @@
    1.40      val (thy3', ind_info) = thy2 |>
    1.41        OldInductivePackage.add_inductive_i false true "" false false false
    1.42          (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
    1.43 -          ((Sign.base_name (Thm.name_of_thm intr), strip_all
    1.44 +          ((Sign.base_name (Thm.get_name intr), strip_all
    1.45              (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
    1.46        Theory.absolute_path;
    1.47      val thy3 = PureThy.hide_thms false
    1.48 -      (map Thm.name_of_thm (#intrs ind_info)) thy3';
    1.49 +      (map Thm.get_name (#intrs ind_info)) thy3';
    1.50  
    1.51      (** realizer for induction rule **)
    1.52  
    1.53 @@ -379,7 +379,7 @@
    1.54               [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
    1.55                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
    1.56          val (thm', thy') = PureThy.store_thm ((space_implode "_"
    1.57 -          (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
    1.58 +          (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy
    1.59        in
    1.60          Extraction.add_realizers_i
    1.61            [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
    1.62 @@ -427,7 +427,7 @@
    1.63             REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
    1.64               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
    1.65          val (thm', thy') = PureThy.store_thm ((space_implode "_"
    1.66 -          (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
    1.67 +          (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy
    1.68        in
    1.69          Extraction.add_realizers_i
    1.70            [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'