--- a/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 12:19:01 2010 +0200
@@ -218,7 +218,7 @@
lthy'
|> Local_Theory.note (eq_abinding, [rec_rule])
|-> (fn (_, rec') =>
- Local_Theory.note ((Binding.qualify true fname (Binding.name "rec"), []), rec'))
+ Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec'))
|> snd
end;
--- a/src/HOL/ex/Fundefs.thy Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy Tue Oct 26 12:19:01 2010 +0200
@@ -222,7 +222,7 @@
then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
else do { ns \<leftarrow> collatz (3 * n + 1); Some (n # ns)})"
-declare collatz.rec[code]
+declare collatz.simps[code]
value "collatz 23"