removed Syntax.binding;
authorwenzelm
Sat Sep 04 21:05:01 1999 +0200 (1999-09-04)
changeset 747443cedde6d52a
parent 7473 fd03510c6841
child 7475 dc4f8d6ee0d2
removed Syntax.binding;
src/Pure/Isar/auto_bind.ML
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Sat Sep 04 21:04:30 1999 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Sat Sep 04 21:05:01 1999 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5      val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @
     1.6        (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
     1.7 -  in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
     1.8 +  in map (fn (s, t) => ((s, 0), t)) env end;
     1.9  
    1.10  fun goal prop = statement_binds ("thesis", prop);
    1.11