src/HOL/Nominal/nominal_datatype.ML
changeset 32957 675c0c7e6a37
parent 32952 aeb1e44fbc19
child 32960 69916a850301
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 16 10:55:07 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Oct 17 00:52:37 2009 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4  
     1.5  fun projections rule =
     1.6    Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     1.7 -  |> map (standard #> RuleCases.save rule);
     1.8 +  |> map (Drule.standard #> RuleCases.save rule);
     1.9  
    1.10  val supp_prod = thm "supp_prod";
    1.11  val fresh_prod = thm "fresh_prod";
    1.12 @@ -313,7 +313,7 @@
    1.13  
    1.14      val unfolded_perm_eq_thms =
    1.15        if length descr = length new_type_names then []
    1.16 -      else map standard (List.drop (split_conj_thm
    1.17 +      else map Drule.standard (List.drop (split_conj_thm
    1.18          (Goal.prove_global thy2 [] []
    1.19            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.20              (map (fn (c as (s, T), x) =>
    1.21 @@ -333,7 +333,7 @@
    1.22  
    1.23      val perm_empty_thms = maps (fn a =>
    1.24        let val permT = mk_permT (Type (a, []))
    1.25 -      in map standard (List.take (split_conj_thm
    1.26 +      in map Drule.standard (List.take (split_conj_thm
    1.27          (Goal.prove_global thy2 [] []
    1.28            (augment_sort thy2 [pt_class_of thy2 a]
    1.29              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.30 @@ -365,7 +365,7 @@
    1.31          val pt_inst = pt_inst_of thy2 a;
    1.32          val pt2' = pt_inst RS pt2;
    1.33          val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    1.34 -      in List.take (map standard (split_conj_thm
    1.35 +      in List.take (map Drule.standard (split_conj_thm
    1.36          (Goal.prove_global thy2 [] []
    1.37             (augment_sort thy2 [pt_class_of thy2 a]
    1.38               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.39 @@ -400,7 +400,7 @@
    1.40          val pt3' = pt_inst RS pt3;
    1.41          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    1.42          val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    1.43 -      in List.take (map standard (split_conj_thm
    1.44 +      in List.take (map Drule.standard (split_conj_thm
    1.45          (Goal.prove_global thy2 [] []
    1.46            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
    1.47               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    1.48 @@ -585,7 +585,7 @@
    1.49        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
    1.50        (perm_indnames ~~ descr);
    1.51  
    1.52 -    fun mk_perm_closed name = map (fn th => standard (th RS mp))
    1.53 +    fun mk_perm_closed name = map (fn th => Drule.standard (th RS mp))
    1.54        (List.take (split_conj_thm (Goal.prove_global thy4 [] []
    1.55          (augment_sort thy4
    1.56            (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
    1.57 @@ -810,7 +810,7 @@
    1.58        let
    1.59          val rep_const = cterm_of thy
    1.60            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
    1.61 -        val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    1.62 +        val dist = Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    1.63          val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
    1.64            ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
    1.65        in
    1.66 @@ -874,7 +874,7 @@
    1.67            let
    1.68              val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
    1.69                simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
    1.70 -          in dist_thm :: standard (dist_thm RS not_sym) ::
    1.71 +          in dist_thm :: Drule.standard (dist_thm RS not_sym) ::
    1.72              prove_distinct_thms p (k, ts)
    1.73            end;
    1.74  
    1.75 @@ -1089,7 +1089,7 @@
    1.76  
    1.77      val finite_supp_thms = map (fn atom =>
    1.78        let val atomT = Type (atom, [])
    1.79 -      in map standard (List.take
    1.80 +      in map Drule.standard (List.take
    1.81          (split_conj_thm (Goal.prove_global thy8 [] []
    1.82             (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
    1.83               (HOLogic.mk_Trueprop
    1.84 @@ -1535,7 +1535,7 @@
    1.85            in
    1.86              (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
    1.87            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
    1.88 -        val ths = map (fn th => standard (th RS mp)) (split_conj_thm
    1.89 +        val ths = map (fn th => Drule.standard (th RS mp)) (split_conj_thm
    1.90            (Goal.prove_global thy11 [] []
    1.91              (augment_sort thy1 pt_cp_sort
    1.92                (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
    1.93 @@ -1567,7 +1567,7 @@
    1.94            (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
    1.95              (rec_fns ~~ rec_fn_Ts)
    1.96        in
    1.97 -        map (fn th => standard (th RS mp)) (split_conj_thm
    1.98 +        map (fn th => Drule.standard (th RS mp)) (split_conj_thm
    1.99            (Goal.prove_global thy11 []
   1.100              (map (augment_sort thy11 fs_cp_sort) fins)
   1.101              (augment_sort thy11 fs_cp_sort
   1.102 @@ -1610,7 +1610,7 @@
   1.103              val y = Free ("y", U);
   1.104              val y' = Free ("y'", U)
   1.105            in
   1.106 -            standard (Goal.prove (ProofContext.init thy11) []
   1.107 +            Drule.standard (Goal.prove (ProofContext.init thy11) []
   1.108                (map (augment_sort thy11 fs_cp_sort)
   1.109                  (finite_prems @
   1.110                     [HOLogic.mk_Trueprop (R $ x $ y),
   1.111 @@ -2055,7 +2055,7 @@
   1.112           ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
   1.113           ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
   1.114           ((Binding.name "rec_fresh", flat rec_fresh_thms), []),
   1.115 -         ((Binding.name "rec_unique", map standard rec_unique_thms), []),
   1.116 +         ((Binding.name "rec_unique", map Drule.standard rec_unique_thms), []),
   1.117           ((Binding.name "recs", rec_thms), [])] ||>
   1.118        Sign.parent_path ||>
   1.119        map_nominal_datatypes (fold Symtab.update dt_infos);