# HG changeset patch
# User haftmann
# Date 1216130530 -7200
# Node ID 8882d47e075fa1dd5d22404cb9bea5b2e2f6ac36
# Parent  b23c9ad0fe7d45484677ec2e35d94cd9edd3be29
tuned

diff -r b23c9ad0fe7d -r 8882d47e075f src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Tue Jul 15 16:02:07 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Tue Jul 15 16:02:10 2008 +0200
@@ -407,7 +407,7 @@
   let
     val thy = Thm.theory_of_thm thm;
     val Const (c, ty) = (fst o strip_comb o fst o Logic.dest_equals
-      o (*ObjectLogic.drop_judgment thy o *)Thm.plain_prop_of) thm;
+      o Thm.plain_prop_of) thm;
   in (c, typscheme thy (c, ty)) end;