# HG changeset patch # User wenzelm # Date 936471901 -7200 # Node ID 43cedde6d52adaf8d1fed0ebc1770ae55b3bac85 # Parent fd03510c6841b3bf72914eabd54b7c57d9e47cda removed Syntax.binding; diff -r fd03510c6841 -r 43cedde6d52a src/Pure/Isar/auto_bind.ML --- 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);