# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255848256 -7200
# Node ID 6ddb2f99be1d81fd592818f143d483f4bd721ea8
# Parent  b054cf6bd17997f4decfe8d32ac62b19a2e83de9
slight fix and tuning

diff -r b054cf6bd179 -r 6ddb2f99be1d QuotMain.thy
--- a/QuotMain.thy	Sun Oct 18 00:52:10 2009 +0200
+++ b/QuotMain.thy	Sun Oct 18 08:44:16 2009 +0200
@@ -284,8 +284,8 @@
   let
     val (fs, tys) = split_list fs_tys
     val ([oty1, oty2], [nty1, nty2]) = split_list tys
-    val oty = Type ("fun", [nty1, oty2])
-    val nty = Type ("fun", [oty1, nty2])
+    val oty = nty1 --> oty2
+    val nty = oty1 --> nty2
     val ftys = map (op -->) tys
   in
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
diff -r b054cf6bd179 -r 6ddb2f99be1d quotient.ML
--- a/quotient.ML	Sun Oct 18 00:52:10 2009 +0200
+++ b/quotient.ML	Sun Oct 18 08:44:16 2009 +0200
@@ -2,6 +2,8 @@
 sig
   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
+  val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
+  val note: binding * thm -> local_theory -> thm * local_theory
 end;
 
 structure Quotient: QUOTIENT =