src/HOL/Nominal/nominal_datatype.ML
changeset 36945 9bec62c10714
parent 36692 54b64d4ad524
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -602,7 +602,7 @@
     1.4          (fn _ => EVERY
     1.5             [indtac rep_induct [] 1,
     1.6              ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
     1.7 -              (symmetric perm_fun_def :: abs_perm))),
     1.8 +              (Thm.symmetric perm_fun_def :: abs_perm))),
     1.9              ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
    1.10          length new_type_names));
    1.11  
    1.12 @@ -927,7 +927,7 @@
    1.13                 simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
    1.14                   constr_defs @ perm_closed_thms)) 1,
    1.15                 TRY (simp_tac (HOL_basic_ss addsimps
    1.16 -                 (symmetric perm_fun_def :: abs_perm)) 1),
    1.17 +                 (Thm.symmetric perm_fun_def :: abs_perm)) 1),
    1.18                 TRY (simp_tac (HOL_basic_ss addsimps
    1.19                   (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
    1.20                      perm_closed_thms)) 1)])
    1.21 @@ -1077,7 +1077,7 @@
    1.22           (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
    1.23           EVERY (map (fn (prem, r) => (EVERY
    1.24             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
    1.25 -            simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
    1.26 +            simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
    1.27              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
    1.28                  (prems ~~ constr_defs))]);
    1.29  
    1.30 @@ -1641,7 +1641,7 @@
    1.31                            fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
    1.32                        supports_fresh) 1,
    1.33                      simp_tac (HOL_basic_ss addsimps
    1.34 -                      [supports_def, symmetric fresh_def, fresh_prod]) 1,
    1.35 +                      [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1,
    1.36                      REPEAT_DETERM (resolve_tac [allI, impI] 1),
    1.37                      REPEAT_DETERM (etac conjE 1),
    1.38                      rtac unique 1,
    1.39 @@ -1655,7 +1655,7 @@
    1.40                      rtac rec_prem 1,
    1.41                      simp_tac (HOL_ss addsimps (fs_name ::
    1.42                        supp_prod :: finite_Un :: finite_prems)) 1,
    1.43 -                    simp_tac (HOL_ss addsimps (symmetric fresh_def ::
    1.44 +                    simp_tac (HOL_ss addsimps (Thm.symmetric fresh_def ::
    1.45                        fresh_prod :: fresh_prems)) 1]
    1.46                   end))
    1.47            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
    1.48 @@ -1746,7 +1746,7 @@
    1.49                 asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
    1.50                  (finite_thss ~~ finite_ctxt_ths) @
    1.51              maps (fn ((_, idxss), elim) => maps (fn idxs =>
    1.52 -              [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
    1.53 +              [full_simp_tac (HOL_ss addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
    1.54                 REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
    1.55                 rtac ex1I 1,
    1.56                 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,