1.1 --- a/src/Pure/Isar/code_unit.ML	Tue Jul 15 16:02:07 2008 +0200
     1.2 +++ b/src/Pure/Isar/code_unit.ML	Tue Jul 15 16:02:10 2008 +0200
     1.3 @@ -407,7 +407,7 @@
     1.4    let
     1.5      val thy = Thm.theory_of_thm thm;
     1.6      val Const (c, ty) = (fst o strip_comb o fst o Logic.dest_equals
     1.7 -      o (*ObjectLogic.drop_judgment thy o *)Thm.plain_prop_of) thm;
     1.8 +      o Thm.plain_prop_of) thm;
     1.9    in (c, typscheme thy (c, ty)) end;
    1.10  
    1.11