src/Pure/Isar/auto_bind.ML
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)))];