1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:52 2010 +0200
     1.3 @@ -295,12 +295,13 @@
     1.4        (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
     1.5        (Symtab.dest (Datatype.get_all thy)));
     1.6      fun check t = (case strip_comb t of
     1.7 -        (Free _, []) => true
     1.8 +        (Var _, []) => true
     1.9 +      | (Free _, []) => true
    1.10        | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
    1.11              (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
    1.12            | _ => false)
    1.13        | _ => false)
    1.14 -  in check end;  
    1.15 +  in check end;
    1.16  
    1.17  fun is_funtype (Type ("fun", [_, _])) = true
    1.18    | is_funtype _ = false;