--- a/src/Pure/Tools/nbe.ML Wed Jul 19 12:11:56 2006 +0200
+++ b/src/Pure/Tools/nbe.ML Wed Jul 19 12:11:57 2006 +0200
@@ -100,8 +100,7 @@
val vtab = var_tab t;
val ty = type_of t;
fun restrain ty t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
- (K NONE) (K NONE)
- [] false ([t], ty) |> fst;
+ (K NONE) (K NONE) Name.context false ([t], ty) |> fst;
val _ = trace (fn () => "Normalized:\n" ^ NBE_Eval.string_of_nterm nt);
val t' = NBE_Codegen.nterm_to_term thy nt;
val _ = trace (fn () =>"Converted back:\n" ^ Display.raw_string_of_term t');