Use generic Simplifier.simp_add attribute instead
authorberghofe
Thu Jan 19 15:45:10 2006 +0100 (2006-01-19)
changeset 187079d6154f76476
parent 18706 1e7562c7afe6
child 18708 4b3dadb4fe33
Use generic Simplifier.simp_add attribute instead
of Simplifier.simp_add_global.
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Jan 19 14:59:55 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jan 19 15:45:10 2006 +0100
     1.3 @@ -201,7 +201,7 @@
     1.4                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
     1.5        in
     1.6            AxClass.add_axclass_i (cl_name, ["HOL.type"])
     1.7 -                [((cl_name^"1", axiom1),[Simplifier.simp_add_global]), 
     1.8 +                [((cl_name^"1", axiom1),[Attrib.theory Simplifier.simp_add]), 
     1.9                   ((cl_name^"2", axiom2),[]),                           
    1.10                   ((cl_name^"3", axiom3),[])] thy                          
    1.11        end) ak_names_types thy6;
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Jan 19 14:59:55 2006 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Jan 19 15:45:10 2006 +0100
     2.3 @@ -428,13 +428,13 @@
     2.4          (List.take (descr, length new_type_names)) |>
     2.5        PureThy.add_thmss
     2.6          [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
     2.7 -          unfolded_perm_eq_thms), [Simplifier.simp_add_global]),
     2.8 +          unfolded_perm_eq_thms), [Attrib.theory Simplifier.simp_add]),
     2.9           ((space_implode "_" new_type_names ^ "_perm_empty",
    2.10 -          perm_empty_thms), [Simplifier.simp_add_global]),
    2.11 +          perm_empty_thms), [Attrib.theory Simplifier.simp_add]),
    2.12           ((space_implode "_" new_type_names ^ "_perm_append",
    2.13 -          perm_append_thms), [Simplifier.simp_add_global]),
    2.14 +          perm_append_thms), [Attrib.theory Simplifier.simp_add]),
    2.15           ((space_implode "_" new_type_names ^ "_perm_eq",
    2.16 -          perm_eq_thms), [Simplifier.simp_add_global])];
    2.17 +          perm_eq_thms), [Attrib.theory Simplifier.simp_add])];
    2.18    
    2.19      (**** Define representing sets ****)
    2.20  
    2.21 @@ -1071,7 +1071,7 @@
    2.22           length new_type_names))
    2.23        end) atoms;
    2.24  
    2.25 -    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];
    2.26 +    val simp_atts = replicate (length new_type_names) [Attrib.theory Simplifier.simp_add];
    2.27  
    2.28      val (_, thy9) = thy8 |>
    2.29        Theory.add_path big_name |>