src/Pure/Tools/nbe_eval.ML
changeset 20596 3950e65f48f8
parent 20105 454f4be984b7
child 20846 5fde744176d7
     1.1 --- a/src/Pure/Tools/nbe_eval.ML	Tue Sep 19 15:21:58 2006 +0200
     1.2 +++ b/src/Pure/Tools/nbe_eval.ML	Tue Sep 19 15:22:03 2006 +0200
     1.3 @@ -88,9 +88,9 @@
     1.4    | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
     1.5  
     1.6  fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
     1.7 -  |	to_term (Var   (name, args))    = apps (V name) (map to_term args)
     1.8 -  |	to_term (BVar  (name, args))    = apps (B name) (map to_term args)
     1.9 -  |	to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
    1.10 +  | to_term (Var   (name, args))    = apps (V name) (map to_term args)
    1.11 +  | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
    1.12 +  | to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
    1.13  
    1.14  (*
    1.15     A typical operation, why functions might be good for, is