1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Apr 21 17:07:44 2009 -0700
1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Wed Apr 22 07:12:21 2009 -0700
1.3 @@ -608,23 +608,22 @@
1.4 in
1.5 thy
1.6 |> Sign.add_path (Long_Name.base_name dname)
1.7 - |> (snd o PureThy.add_thmss [
1.8 - ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
1.9 - ((Binding.name "exhaust" , [exhaust] ), []),
1.10 - ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]),
1.11 - ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
1.12 - ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
1.13 - ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
1.14 - ((Binding.name "sel_rews", sel_rews), [Simplifier.simp_add]),
1.15 - ((Binding.name "dis_rews", dis_rews), [Simplifier.simp_add]),
1.16 - ((Binding.name "pat_rews", pat_rews), [Simplifier.simp_add]),
1.17 - ((Binding.name "dist_les", dist_les), [Simplifier.simp_add]),
1.18 - ((Binding.name "dist_eqs", dist_eqs), [Simplifier.simp_add]),
1.19 - ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
1.20 - ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
1.21 - ((Binding.name "copy_rews", copy_rews), [Simplifier.simp_add]),
1.22 - ((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])
1.23 - ])
1.24 + |> snd o PureThy.add_thmss [
1.25 + ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
1.26 + ((Binding.name "exhaust" , [exhaust] ), []),
1.27 + ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]),
1.28 + ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]),
1.29 + ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]),
1.30 + ((Binding.name "con_rews" , con_rews ), [Simplifier.simp_add]),
1.31 + ((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]),
1.32 + ((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]),
1.33 + ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]),
1.34 + ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]),
1.35 + ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]),
1.36 + ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
1.37 + ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
1.38 + ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]),
1.39 + ((Binding.name "match_rews", mat_rews ), [Simplifier.simp_add])]
1.40 |> Sign.parent_path
1.41 |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
1.42 pat_rews @ dist_les @ dist_eqs @ copy_rews)
1.43 @@ -1004,14 +1003,14 @@
1.44 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
1.45
1.46 in thy |> Sign.add_path comp_dnam
1.47 - |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
1.48 - ("take_rews" , take_rews ),
1.49 - ("take_lemmas", take_lemmas),
1.50 - ("finites" , finites ),
1.51 - ("finite_ind", [finite_ind]),
1.52 - ("ind" , [ind ]),
1.53 - ("coind" , [coind ])])))
1.54 - |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts))))
1.55 + |> snd o PureThy.add_thmss [
1.56 + ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]),
1.57 + ((Binding.name "take_lemmas", take_lemmas ), []),
1.58 + ((Binding.name "finites" , finites ), []),
1.59 + ((Binding.name "finite_ind" , [finite_ind]), []),
1.60 + ((Binding.name "ind" , [ind] ), []),
1.61 + ((Binding.name "coind" , [coind] ), [])]
1.62 + |> snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))
1.63 |> Sign.parent_path |> pair take_rews
1.64 end; (* let *)
1.65 end; (* local *)