Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/datatype_rep_proofs.ML
changeset 26626 c6231d64d264
parent 26531 96e82c7861fa
child 26711 3a478bfa1650 
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 10 20:54:18 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Apr 12 17:00:35 2008 +0200
@@ -359,7 +359,8 @@
 
     fun mk_funs_inv thm =
       let
-        val {thy, prop, ...} = rep_thm thm;
+        val thy = Thm.theory_of_thm thm;
+        val prop = Thm.prop_of thm;
         val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
           (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
         val used = add_term_tfree_names (a, []);
isabelle