--- a/src/ZF/Tools/datatype_package.ML Sat Mar 07 22:16:50 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Mar 07 22:17:25 2009 +0100
@@ -245,14 +245,14 @@
fun add_recursor thy =
if need_recursor then
thy |> Sign.add_consts_i
- [(recursor_base_name, recursor_typ, NoSyn)]
+ [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
|> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
else thy;
val (con_defs, thy0) = thy_path
|> Sign.add_consts_i
- ((case_base_name, case_typ, NoSyn) ::
- map #1 (List.concat con_ty_lists))
+ (map (fn (c, T, mx) => (Binding.name c, T, mx))
+ ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
|> PureThy.add_defs false
(map (Thm.no_attributes o apfst Binding.name)
(case_def ::
@@ -302,7 +302,7 @@
(*** Prove the recursor theorems ***)
- val recursor_eqns = case try (Thm.get_def thy1) recursor_base_name of
+ val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
NONE => (writeln " [ No recursion operator ]";
[])
| SOME recursor_def =>