src/Pure/thm.ML
changeset 432 0d1071ac599c
parent 427 4ce2ce940faf
child 446 3ee5c9314efe
equal deleted inserted replaced
431:da3d07d4349b 432:0d1071ac599c
  1190   | lextermord([],[]) = EQUAL
  1190   | lextermord([],[]) = EQUAL
  1191   | lextermord _ = error("lextermord");
  1191   | lextermord _ = error("lextermord");
  1192 
  1192 
  1193 fun termless tu = (termord tu = LESS);
  1193 fun termless tu = (termord tu = LESS);
  1194 
  1194 
  1195 fun check_conv(thm as Thm{hyps,prop,...}, prop0) =
  1195 fun check_conv(thm as Thm{hyps,prop,sign,...}, prop0) =
  1196   let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None)
  1196   let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm;
       
  1197                    trace_term "Should have proved" sign prop0;
       
  1198                    None)
  1197       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
  1199       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
  1198   in case prop of
  1200   in case prop of
  1199        Const("==",_) $ lhs $ rhs =>
  1201        Const("==",_) $ lhs $ rhs =>
  1200          if (lhs = lhs0) orelse
  1202          if (lhs = lhs0) orelse
  1201             (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
  1203             (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)