Mercurial Mercurial > hg > nominal2 / 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.
Quot/quotient_def.ML
changeset 854 5961edda27d7
parent 833 129caba33c03
child 856 433f7c17255f 
--- a/Quot/quotient_def.ML	Tue Jan 12 10:59:51 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 13 00:45:28 2010 +0100
@@ -40,8 +40,8 @@
 let
   val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
   val qconst_bname = Binding.name lhs_str;
-  val absrep_trm = (absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty)) $ rhs
-  val prop = Logic.mk_equals (lhs, absrep_trm)
+  val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
+  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'
nominal2