changeset 24976 | 821628d16552 |
parent 24971 | 4d006b03aa4a |
child 25110 | 7253d331e9fc |
--- a/src/Tools/code/code_package.ML Thu Oct 11 18:58:34 2007 +0200 +++ b/src/Tools/code/code_package.ML Thu Oct 11 19:10:17 2007 +0200 @@ -157,7 +157,7 @@ fun mk_codeprops thy all_cs sel_cs = let - fun select (thmref, thm) = case try (Drule.unvarify o Drule.zero_var_indexes) thm + fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm of NONE => NONE | SOME thm => let val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;