changeset 40844 | 5895c525739d |
parent 40627 | becf5d5187cc |
child 40919 | cdb34f393a7e |
--- a/src/Pure/codegen.ML Wed Dec 01 15:02:39 2010 +0100 +++ b/src/Pure/codegen.ML Wed Dec 01 15:03:44 2010 +0100 @@ -664,7 +664,7 @@ NONE => let val _ = message ("expanding definition of " ^ s); - val (Ts, _) = strip_type U; + val Ts = binder_types U; val (args', rhs') = if not (null args) orelse null Ts then (args, rhs) else let val v = Free (new_name rhs "x", hd Ts)