src/HOL/Tools/datatype_rep_proofs.ML
changeset 16287 7a03b4b4df67
parent 15574 b1d1b5bfc464
child 16431 90c9b8bb3b66
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Jun 05 23:07:24 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Jun 05 23:07:25 2005 +0200
     1.3 @@ -388,8 +388,8 @@
     1.4      fun mk_funs_inv thm =
     1.5        let
     1.6          val {sign, prop, ...} = rep_thm thm;
     1.7 -        val (_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
     1.8 -          (_ $ (_ $ (r $ (a $ _)) $ _)), _) = Type.freeze_thaw prop;
     1.9 +        val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
    1.10 +          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
    1.11          val used = add_term_tfree_names (a, []);
    1.12  
    1.13          fun mk_thm i =