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/Prod.ML
changeset 8100 6186ee807f2e
parent 7958 f531589c9fc1
child 8157 b1a458416c92 
--- a/src/HOL/Prod.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Prod.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -171,7 +171,7 @@
 	(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
 	(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
   fun simproc name patstr = Simplifier.mk_simproc name 
-		[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termTVar)];
+		[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termT)];
 
   val beta_patstr = "split f z";
   val  eta_patstr = "split f";
isabelle