src/Pure/raw_simplifier.ML
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -1293,7 +1293,7 @@
     1.4      val thy = Proof_Context.theory_of raw_ctxt;
     1.5  
     1.6      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
     1.7 -    val {maxidx, ...} = Thm.rep_cterm ct;
     1.8 +    val maxidx = Thm.maxidx_of_cterm ct;
     1.9      val _ =
    1.10        Theory.subthy (Thm.theory_of_cterm ct, thy) orelse
    1.11          raise CTERM ("rewrite_cterm: bad background theory", [ct]);