--- a/src/HOL/Tools/inductive_realizer.ML Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Aug 24 14:42:24 2008 +0200
@@ -211,7 +211,7 @@
let
val fs = map (fn (rule, (ivs, intr)) =>
fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
- in if dummy then Const ("arbitrary",
+ in if dummy then Const ("HOL.default_class.default",
HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
else fs
end) (premss ~~ dummies);
@@ -438,7 +438,7 @@
val r = if null Ps then Extraction.nullt
else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
(if dummy then
- [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
+ [Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))]
else []) @
map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
[Bound (length prems)]));