src/HOL/Tools/inductive_package.ML
changeset 18358 0a733e11021a
parent 18330 444f16d232a2
child 18377 0e1d025d57b3
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Dec 06 06:22:14 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 06 09:04:09 2005 +0100
     1.3 @@ -451,7 +451,7 @@
     1.4      fun cases_spec name elim thy =
     1.5        thy
     1.6        |> Theory.add_path (Sign.base_name name)
     1.7 -      |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
     1.8 +      |> (fst o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
     1.9        |> Theory.parent_path;
    1.10      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    1.11  
    1.12 @@ -750,7 +750,7 @@
    1.13      val def_terms = fp_def_term :: (if length cs < 2 then [] else
    1.14        map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
    1.15  
    1.16 -    val (thy', [fp_def :: rec_sets_defs]) =
    1.17 +    val ([fp_def :: rec_sets_defs], thy') =
    1.18        thy
    1.19        |> cond_declare_consts declare_consts cs paramTs cnames
    1.20        |> (if length cs < 2 then I