src/HOL/Orderings.thy
changeset 16861 7446b4be013b
parent 16796 140f1e0ea846
child 17012 036c46df9576
--- a/src/HOL/Orderings.thy	Fri Jul 15 15:44:11 2005 +0200
+++ b/src/HOL/Orderings.thy	Fri Jul 15 15:44:15 2005 +0200
@@ -545,7 +545,7 @@
 print_translation {*
 let
   fun mk v v' q n P =
-    if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
+    if v=v' andalso not (v mem (map fst (Term.add_frees n [])))
     then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
   fun all_tr' [Const ("_bound",_) $ Free (v,_),
                Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =