changeset 32748 | 887c68b70f7d |
parent 32745 | 192d58483fdf |
child 32749 | 3282c12a856c |
--- a/src/HOL/Tools/record.ML Fri Sep 11 15:57:16 2009 +1000 +++ b/src/HOL/Tools/record.ML Fri Sep 11 18:03:30 2009 +1000 @@ -1721,8 +1721,7 @@ [("ext_inject", inject), ("ext_induct", induct), ("ext_surjective", surject), - ("ext_split", split_meta), - ("ext_def", ext_def)] + ("ext_split", split_meta)] in (thm_thy,extT,induct',inject',split_meta',ext_def') end;