1844 if simprem then try_botc mss (shyps,hyps,maxidx,s,ders) |
1844 if simprem then try_botc mss (shyps,hyps,maxidx,s,ders) |
1845 else (shyps,hyps,0,s,ders); |
1845 else (shyps,hyps,0,s,ders); |
1846 val maxidx1 = maxidx_of_term s1 |
1846 val maxidx1 = maxidx_of_term s1 |
1847 val mss1 = |
1847 val mss1 = |
1848 if not useprem then mss else |
1848 if not useprem then mss else |
1849 if maxidx1 <> ~1 then (prtm_warning |
1849 if maxidx1 <> ~1 then (trace_term_warning |
1850 "Cannot add premise as rewrite rule because it contains (type) unknowns:" |
1850 "Cannot add premise as rewrite rule because it contains (type) unknowns:" |
1851 sign s1; mss) |
1851 sign s1; mss) |
1852 else let val thm = assume (Cterm{sign=sign, t=s1, |
1852 else let val thm = assume (Cterm{sign=sign, t=s1, |
1853 T=propT, maxidx=maxidx1}) |
1853 T=propT, maxidx=maxidx1}) |
1854 in add_simps(add_prems(mss,[thm]), mk_rews thm) end |
1854 in add_simps(add_prems(mss,[thm]), mk_rews thm) end |