Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/normarith.ML
changeset 81954 6f2bcdfa9a19
parent 74626 9a1f4a7ddf9e 
--- a/src/HOL/Analysis/normarith.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Analysis/normarith.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -359,7 +359,7 @@
   val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
   val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1)
   val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
-  val cps = map (swap o Thm.dest_equals) (cprems_of th11)
+  val cps = map (swap o Thm.dest_equals) (Thm.cprems_of th11)
   val th12 = Drule.instantiate_normalize (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cps)) th11
   val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
  in hd (Variable.export ctxt' ctxt [th13])
isabelle