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/Integ/presburger.ML
changeset 20194 c9dbce9a23a1
parent 20053 7f32ce6354d6
child 20255 5a8410198a33 
--- a/src/HOL/Integ/presburger.ML	Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Integ/presburger.ML	Tue Jul 25 21:18:00 2006 +0200
@@ -65,7 +65,7 @@
 	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
 
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
-  let val (xn1,p1) = variant_abs (xn,xT,p)
+  let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
   in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
 
 fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
isabelle