src/Pure/thm.ML
changeset 900 8e22076cd3ca
parent 898 4f9c8503d1c5
child 922 196ca0973a6d
equal deleted inserted replaced
899:516f9e349a16 900:8e22076cd3ca
  1054                     eq_set(add_term_vars(t,[]), add_term_vars(u,[]))
  1054                     eq_set(add_term_vars(t,[]), add_term_vars(u,[]))
  1055 
  1055 
  1056 (*simple test for looping rewrite*)
  1056 (*simple test for looping rewrite*)
  1057 fun loops sign prems (lhs,rhs) =
  1057 fun loops sign prems (lhs,rhs) =
  1058   is_Var(lhs) orelse
  1058   is_Var(lhs) orelse
  1059   (is_Free(lhs) andalso (lhs mem (foldr add_term_frees (prems,[])))) orelse
  1059   (is_Free(lhs) andalso (lhs mem (foldr add_term_frees (rhs::prems,[])))) orelse
  1060   (null(prems) andalso
  1060   (null(prems) andalso
  1061    Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
  1061    Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
  1062 
  1062 
  1063 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
  1063 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
  1064   let val prems = Logic.strip_imp_prems prop
  1064   let val prems = Logic.strip_imp_prems prop