changeset 27610 | 8882d47e075f |
parent 27582 | 367aff8d7ffd |
child 28015 | 11635f41abc1 |
--- 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;