src/Pure/Isar/auto_bind.ML
changeset 7474 43cedde6d52a
parent 7452 c2289eabf706
child 7599 40b7f7f51208
--- a/src/Pure/Isar/auto_bind.ML	Sat Sep 04 21:04:30 1999 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Sat Sep 04 21:05:01 1999 +0200
@@ -25,7 +25,7 @@
 
     val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @
       (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
-  in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
+  in map (fn (s, t) => ((s, 0), t)) env end;
 
 fun goal prop = statement_binds ("thesis", prop);