src/HOL/Tools/recdef_package.ML
changeset 24712 64ed05609568
parent 24624 b8383b1bbae3
child 24867 e5b55d7be9bb
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Sep 25 15:34:35 2007 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 25 17:06:14 2007 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4  
     1.5      val ((simps' :: rules', [induct']), thy) =
     1.6        thy
     1.7 -      |> Theory.add_path bname
     1.8 +      |> Sign.add_path bname
     1.9        |> PureThy.add_thmss
    1.10          ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    1.11        ||>> PureThy.add_thms [(("induct", induct), [])];
    1.12 @@ -223,7 +223,7 @@
    1.13      val thy =
    1.14        thy
    1.15        |> put_recdef name result
    1.16 -      |> Theory.parent_path;
    1.17 +      |> Sign.parent_path;
    1.18    in (thy, result) end;
    1.19  
    1.20  val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
    1.21 @@ -245,9 +245,9 @@
    1.22      val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
    1.23      val ([induct_rules'], thy3) =
    1.24        thy2
    1.25 -      |> Theory.add_path bname
    1.26 +      |> Sign.add_path bname
    1.27        |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
    1.28 -      ||> Theory.parent_path;
    1.29 +      ||> Sign.parent_path;
    1.30    in (thy3, {induct_rules = induct_rules'}) end;
    1.31  
    1.32  val defer_recdef = gen_defer_recdef Tfl.defer IsarCmd.apply_theorems;