changeset 35625 | 9c818cab0dd0 |
parent 33386 | ff29d1549aca |
child 41489 | 8e2b8649507d |
--- a/src/Pure/Isar/auto_bind.ML Sun Mar 07 11:57:16 2010 +0100 +++ b/src/Pure/Isar/auto_bind.ML Sun Mar 07 12:19:47 2010 +0100 @@ -23,7 +23,7 @@ val thisN = "this"; val assmsN = "assms"; -fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl; +fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl; fun statement_binds thy name prop = [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];