--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Apr 08 14:05:31 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Apr 08 14:20:57 2011 +0200
@@ -47,10 +47,9 @@
val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
in
Function.add_function
- (map (fn (name, T) =>
- Syntax.no_syn (Binding.conceal (Binding.name name), SOME T))
- (names ~~ Ts))
- (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
+ (map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn))
+ (names ~~ Ts))
+ (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
Function_Common.default_config pat_completeness_auto
#> snd
#> Local_Theory.restore