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.ML
changeset 719 a9e55e1ef64c
parent 685 b12f0321dfb0 
--- a/Quot/quotient.ML	Fri Dec 11 16:32:40 2009 +0100
+++ b/Quot/quotient.ML	Fri Dec 11 17:19:38 2009 +0100
@@ -132,12 +132,12 @@
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
   (* ABS and REP definitions *)
-  val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
-  val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
+  val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT )
+  val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT )
   val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
   val REP_trm = Syntax.check_term lthy1 (REP_const $ rep)
-  val ABS_name = Binding.prefix_name "ABS_" qty_name
-  val REP_name = Binding.prefix_name "REP_" qty_name
+  val ABS_name = Binding.prefix_name "abs_" qty_name
+  val REP_name = Binding.prefix_name "rep_" qty_name
   val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
          lthy1 |> define (ABS_name, NoSyn, ABS_trm)
                ||>> define (REP_name, NoSyn, REP_trm)
nominal2