--- a/Quot/Examples/FSet.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -26,20 +26,20 @@
   apply(rule equivp_list_eq)
   done
 
-quotient_def 
-  EMPTY :: "'a fset"
+quotient_def
+  EMPTY :: "EMPTY :: 'a fset"
 where
-  "EMPTY \<equiv> ([]::'a list)"
+  "[]::'a list"
 
-quotient_def 
-  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+quotient_def
+  INSERT :: "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
-  "INSERT \<equiv> op #"
+  "op #"
 
-quotient_def 
-  FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+quotient_def
+  FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
-  "FUNION \<equiv> (op @)"
+  "op @"
 
 fun
   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
@@ -53,10 +53,10 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
-quotient_def 
-  CARD :: "'a fset \<Rightarrow> nat"
+quotient_def
+  CARD :: "CARD :: 'a fset \<Rightarrow> nat"
 where
-  "CARD \<equiv> card1"
+  "card1"
 
 (* text {*
  Maybe make_const_def should require a theorem that says that the particular lifted function
@@ -117,19 +117,19 @@
   done
 
 quotient_def
-  IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+  IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 where
-  "IN \<equiv> membship"
+  "membship"
 
-quotient_def 
-  FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
+quotient_def
+  FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
-  "FOLD \<equiv> fold1"
+  "fold1"
 
-quotient_def 
-  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+quotient_def
+  fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
-  "fmap \<equiv> map"
+  "map"
 
 lemma memb_rsp:
   fixes z
@@ -318,14 +318,14 @@
   by (rule equivp_list_eq)
 
 quotient_def
-  EMPTY2 :: "'a fset2"
+  EMPTY2 :: "EMPTY2 :: 'a fset2"
 where
-  "EMPTY2 \<equiv> ([]::'a list)"
+  "[]::'a list"
 
 quotient_def
-  INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+  INSERT2 :: "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 where
-  "INSERT2 \<equiv> op #"
+  "op #"
 
 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (lifting list_induct_part)
@@ -336,14 +336,14 @@
 done
 
 quotient_def
-  fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+  fset_rec::"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
-  "fset_rec \<equiv> list_rec"
+  "list_rec"
 
 quotient_def
-  fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+  fset_case::"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
-  "fset_case \<equiv> list_case"
+  "list_case"
 
 (* Probably not true without additional assumptions about the function *)
 lemma list_rec_rsp[quot_respect]:

--- a/Quot/Examples/IntEx.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx
-imports "../QuotList" "../QuotProd" Nitpick
+imports "../QuotProd" "../QuotList"
 begin
 
 fun
@@ -21,56 +21,35 @@
 print_theorems
 print_quotients
 
-quotient_def 
-  ZERO::"my_int"
+quotient_def
+  ZERO::"zero :: my_int"
 where
-  "ZERO \<equiv> (0::nat, 0::nat)"
-
-ML {* print_qconstinfo @{context} *}
-
-term ZERO
-thm ZERO_def
-
-ML {* prop_of @{thm ZERO_def} *}
+  "(0::nat, 0::nat)"
 
-ML {* separate *}
-
-quotient_def 
-  ONE::"my_int"
+quotient_def
+  ONE::"one :: my_int"
 where
-  "ONE \<equiv> (1::nat, 0::nat)"
-
-ML {* print_qconstinfo @{context} *}
-
-term ONE
-thm ONE_def
+  "(1::nat, 0::nat)"
 
 fun
   my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def 
-  PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+quotient_def
+  PLUS::"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
-  "PLUS \<equiv> my_plus"
-
-term my_plus
-term PLUS
-thm PLUS_def
+  "my_plus"
 
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "my_neg (x, y) = (y, x)"
 
-quotient_def 
-  NEG::"my_int \<Rightarrow> my_int"
+quotient_def
+  NEG::"NEG :: my_int \<Rightarrow> my_int"
 where
-  "NEG \<equiv> my_neg"
-
-term NEG
-thm NEG_def
+  "my_neg"
 
 definition
   MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
@@ -82,13 +61,11 @@
 where
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def 
-  MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+quotient_def
+  MULT::"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
-  "MULT \<equiv> my_mult"
+  "my_mult"
 
-term MULT
-thm MULT_def
 
 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
 fun
@@ -96,10 +73,10 @@
 where
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def 
-  LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
+quotient_def
+  LE :: "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
 where
-  "LE \<equiv> my_le"
+  "my_le"
 
 term LE
 thm LE_def

--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -20,34 +20,27 @@
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
 
-quotient_def 
-  zero_qnt::"int"
+quotient_def
+  zero_int::"0 :: int"
 where
-  "zero_qnt \<equiv> (0::nat, 0::nat)"
-
-definition  Zero_int_def[code del]: 
-  "0 = zero_qnt"
+  "(0::nat, 0::nat)"
 
-quotient_def 
-  one_qnt::"int"
+thm zero_int_def
+
+quotient_def
+  one_int::"1 :: int"
 where
-  "one_qnt \<equiv> (1::nat, 0::nat)"
-
-definition One_int_def[code del]:
-  "1 = one_qnt"
+  "(1::nat, 0::nat)"
 
 fun
   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def 
-  plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+quotient_def
+  plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)"
 where
-  "plus_qnt \<equiv> plus_raw"
-
-definition add_int_def[code del]:
-  "z + w = plus_qnt z w"
+  "plus_raw"
 
 fun
   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -55,51 +48,42 @@
   "minus_raw (x, y) = (y, x)"
 
 quotient_def
-  minus_qnt::"int \<Rightarrow> int"
+  uminus_int::"(uminus :: (int \<Rightarrow> int))"
 where
-  "minus_qnt \<equiv> minus_raw"
-
-definition minus_int_def [code del]:
-    "- z = minus_qnt z"
+  "minus_raw"
 
 definition
-  diff_int_def [code del]:  "z - w = z + (-w::int)"
+  minus_int_def [code del]:  "z - w = z + (-w::int)"
 
 fun
-  mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+  times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
-  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+  "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def 
-  mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+quotient_def
+  times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)"
 where
-  "mult_qnt \<equiv> mult_raw"
-
-definition
-  mult_int_def [code del]: "z * w = mult_qnt z w"
+  "times_raw"
 
 fun
-  le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+  less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
-  "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
+  "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def 
-  le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
+quotient_def
+  less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
 where
-  "le_qnt \<equiv> le_raw"
-
-definition
-  le_int_def [code del]:
-   "z \<le> w = le_qnt z w"
+  "less_eq_raw"
 
 definition
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
 
 definition
-  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+  abs_int_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
 
 definition
-  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+  sgn_int_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
 
 instance ..
 
@@ -114,13 +98,13 @@
   by auto
 
 lemma mult_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw"
 apply(auto)
 apply(simp add: algebra_simps)
 sorry
 
-lemma le_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
+lemma less_eq_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw"
 by auto
 
 lemma plus_assoc_raw:
@@ -139,21 +123,21 @@
   shows "plus_raw (minus_raw i) i \<approx> (0, 0)"
 by (cases i) (simp)
 
-lemma mult_assoc_raw:
-  shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
+lemma times_assoc_raw:
+  shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)"
 by (cases i, cases j, cases k) 
    (simp add: algebra_simps)
 
-lemma mult_sym_raw:
-  shows "mult_raw i j \<approx> mult_raw j i"
+lemma times_sym_raw:
+  shows "times_raw i j \<approx> times_raw j i"
 by (cases i, cases j) (simp add: algebra_simps)
 
-lemma mult_one_raw:
-  shows "mult_raw  (1, 0) i \<approx> i"
+lemma times_one_raw:
+  shows "times_raw  (1, 0) i \<approx> i"
 by (cases i) (simp)
 
-lemma mult_plus_comm_raw:
-  shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
+lemma times_plus_comm_raw:
+  shows "times_raw (plus_raw i j) k \<approx> plus_raw (times_raw i k) (times_raw j k)"
 by (cases i, cases j, cases k) 
    (simp add: algebra_simps)
 
@@ -163,38 +147,36 @@
 
 text{*The integers form a @{text comm_ring_1}*}
 
+print_quotconsts
+ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *}
+
+ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *}
+ML {* @{term "0 :: int"} *}
+
+thm plus_assoc_raw
 
 instance int :: comm_ring_1
 proof
   fix i j k :: int
   show "(i + j) + k = i + (j + k)"
-    unfolding add_int_def
-    by (lifting plus_assoc_raw)
+     by (lifting plus_assoc_raw)
   show "i + j = j + i" 
-    unfolding add_int_def
     by (lifting plus_sym_raw)
   show "0 + i = (i::int)"
-    unfolding add_int_def Zero_int_def 
     by (lifting plus_zero_raw)
   show "- i + i = 0"
-    unfolding add_int_def minus_int_def Zero_int_def 
     by (lifting plus_minus_zero_raw)
   show "i - j = i + - j"
-    by (simp add: diff_int_def)
+    by (simp add: minus_int_def)
   show "(i * j) * k = i * (j * k)"
-    unfolding mult_int_def 
-    by (lifting mult_assoc_raw)
+    by (lifting times_assoc_raw)
   show "i * j = j * i"
-    unfolding mult_int_def 
-    by (lifting mult_sym_raw)
+    by (lifting times_sym_raw)
   show "1 * i = i"
-    unfolding mult_int_def One_int_def
-    by (lifting mult_one_raw)
+    by (lifting times_one_raw)
   show "(i + j) * k = i * k + j * k"
-    unfolding mult_int_def add_int_def
-    by (lifting mult_plus_comm_raw)
+    by (lifting times_plus_comm_raw)
   show "0 \<noteq> (1::int)"
-    unfolding Zero_int_def One_int_def
     by (lifting one_zero_distinct)
 qed
 
@@ -202,27 +184,26 @@
 thm of_nat_def
 
 lemma int_def: "of_nat m = ABS_int (m, 0)"
-apply(induct m) 
-apply(simp add: Zero_int_def zero_qnt_def)
+apply(induct m)
+apply(simp add: zero_int_def)
 apply(simp)
-apply(simp add: add_int_def One_int_def)
-apply(simp add: plus_qnt_def one_qnt_def)
+apply(simp add: plus_int_def one_int_def)
 oops
 
 lemma le_antisym_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
+  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
 by (cases i, cases j) (simp)
 
 lemma le_refl_raw:
-  shows "le_raw i i"
+  shows "less_eq_raw i i"
 by (cases i) (simp)
 
 lemma le_trans_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
+  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j k \<Longrightarrow> less_eq_raw i k"
 by (cases i, cases j, cases k) (simp)
 
 lemma le_cases_raw:
-  shows "le_raw i j \<or> le_raw j i"
+  shows "less_eq_raw i j \<or> less_eq_raw j i"
 by (cases i, cases j) 
    (simp add: linorder_linear)
 
@@ -230,18 +211,14 @@
 proof
   fix i j k :: int
   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
-    unfolding le_int_def
     by (lifting le_antisym_raw)
   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
     by (auto simp add: less_int_def dest: antisym) 
   show "i \<le> i"
-    unfolding le_int_def
     by (lifting le_refl_raw)
   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
-    unfolding le_int_def
     by (lifting le_trans_raw)
   show "i \<le> j \<or> j \<le> i"
-    unfolding le_int_def
     by (lifting le_cases_raw)
 qed
 
@@ -261,7 +238,7 @@
 end
 
 lemma le_plus_raw:
-  shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
+  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw (plus_raw k i) (plus_raw k j)"
 by (cases i, cases j, cases k) (simp)
 
 
@@ -269,13 +246,12 @@
 proof
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
-    unfolding le_int_def add_int_def
     by (lifting le_plus_raw)
 qed
 
 lemma test:
-  "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
-    \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
+  "\<lbrakk>less_eq_raw i j \<and> \<not>i \<approx> j; less_eq_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
+    \<Longrightarrow> less_eq_raw (times_raw k i) (times_raw k j) \<and> \<not>times_raw k i \<approx> times_raw k j"
 apply(cases i, cases j, cases k)
 apply(auto simp add: algebra_simps)
 sorry
@@ -286,19 +262,19 @@
 proof
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
-    unfolding mult_int_def le_int_def less_int_def Zero_int_def
+    unfolding less_int_def
     by (lifting test)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
-    by (simp only: zabs_def)
+    by (simp only: abs_int_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
-    by (simp only: zsgn_def)
+    by (simp only: sgn_int_def)
 qed
 
 instance int :: lordered_ring
 proof  
   fix k :: int
   show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
+    by (auto simp add: sup_int_def abs_int_def less_minus_self_iff [symmetric])
 qed
 
 lemmas int_distrib =
@@ -414,4 +390,4 @@
   Bit0_Pls Bit1_Min
 *)
 
-end
\ No newline at end of file
+end

--- a/Quot/Examples/LFex.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/LFex.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -82,51 +82,51 @@
 
 print_quotients
 
-quotient_def 
-  TYP :: "KIND"
+quotient_def
+  TYP :: "TYP :: KIND"
 where
-  "TYP \<equiv> Type"
+  "Type"
 
-quotient_def 
-  KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
+quotient_def
+  KPI :: "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
 where
-  "KPI \<equiv> KPi"
+  "KPi"
 
-quotient_def 
-  TCONST :: "ident \<Rightarrow> TY"
+quotient_def
+  TCONST :: "TCONST :: ident \<Rightarrow> TY"
 where
-  "TCONST \<equiv> TConst"
+  "TConst"
 
-quotient_def 
-  TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY"
+quotient_def
+  TAPP :: "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
 where
-  "TAPP \<equiv> TApp"
+  "TApp"
 
-quotient_def 
-  TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
+quotient_def
+  TPI :: "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
 where
-  "TPI \<equiv> TPi"
+  "TPi"
 
 (* FIXME: does not work with CONST *)
-quotient_def 
-  CONS :: "ident \<Rightarrow> TRM"
+quotient_def
+  CONS :: "CONS :: ident \<Rightarrow> TRM"
 where
-  "CONS \<equiv> Const"
+  "Const"
 
-quotient_def 
-  VAR :: "name \<Rightarrow> TRM"
+quotient_def
+  VAR :: "VAR :: name \<Rightarrow> TRM"
 where
-  "VAR \<equiv> Var"
+  "Var"
 
-quotient_def 
-  APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM"
+quotient_def
+  APP :: "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
 where
-  "APP \<equiv> App"
+  "App"
 
-quotient_def 
-  LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
+quotient_def
+  LAM :: "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
 where
-  "LAM \<equiv> Lam"
+  "Lam"
 
 thm TYP_def
 thm KPI_def
@@ -139,20 +139,20 @@
 thm LAM_def
 
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
-quotient_def 
-  FV_kind :: "KIND \<Rightarrow> name set"
+quotient_def
+  FV_kind :: "FV_kind :: KIND \<Rightarrow> name set"
 where
-  "FV_kind \<equiv> fv_kind"
+  "fv_kind"
 
-quotient_def 
-  FV_ty :: "TY \<Rightarrow> name set"
+quotient_def
+  FV_ty :: "FV_ty :: TY \<Rightarrow> name set"
 where
-  "FV_ty \<equiv> fv_ty"
+  "fv_ty"
 
-quotient_def 
-  FV_trm :: "TRM \<Rightarrow> name set"
+quotient_def
+  FV_trm :: "FV_trm :: TRM \<Rightarrow> name set"
 where
-  "FV_trm \<equiv> fv_trm"
+  "fv_trm"
 
 thm FV_kind_def
 thm FV_ty_def
@@ -165,20 +165,20 @@
     perm_trm  \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"     (unchecked) 
 begin
 
-quotient_def 
-  perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
+quotient_def
+  perm_kind :: "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
 where
-  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
+  "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
 
-quotient_def 
-  perm_ty :: "'x prm \<Rightarrow> TY \<Rightarrow> TY"
+quotient_def
+  perm_ty :: "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
 where
-  "perm_ty \<equiv> (perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
+  "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
 
-quotient_def 
-  perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+quotient_def
+  perm_trm :: "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
 where
-  "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
+  "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 end
 
@@ -253,9 +253,6 @@
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply(lifting akind_aty_atrm.induct)
-(* FIXME: with overloaded definitions *)
-apply(fold perm_kind_def perm_ty_def perm_trm_def)
-apply(cleaning)
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}

--- a/Quot/Examples/LamEx.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -56,29 +56,29 @@
 
 print_quotients
 
-quotient_def 
-  Var :: "name \<Rightarrow> lam"
+quotient_def
+  Var :: "Var :: name \<Rightarrow> lam"
 where
-  "Var \<equiv> rVar"
+  "rVar"
 
-quotient_def 
-  App :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+quotient_def
+  App :: "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
 where
-  "App \<equiv> rApp"
+  "rApp"
 
-quotient_def 
-  Lam :: "name \<Rightarrow> lam \<Rightarrow> lam"
+quotient_def
+  Lam :: "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
 where
-  "Lam \<equiv> rLam"
+  "rLam"
 
 thm Var_def
 thm App_def
 thm Lam_def
 
-quotient_def 
-  fv :: "lam \<Rightarrow> name set"
+quotient_def
+  fv :: "fv :: lam \<Rightarrow> name set"
 where
-  "fv \<equiv> rfv"
+  "rfv"
 
 thm fv_def
 
@@ -88,10 +88,10 @@
   perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
 begin
 
-quotient_def 
-  perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
+quotient_def
+  perm_lam :: "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
 where
-  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"
+  "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 end
 
@@ -244,4 +244,4 @@
   apply(simp add: var_supp)
   done
 
-end
\ No newline at end of file
+end

--- a/Quot/QuotMain.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -398,21 +398,25 @@
        in 
          if rel' = rel then rtrm else raise exc
        end  
-  | (_, Const (s, _)) =>
+  | (_, Const (s, Type(st, _))) =>
        let 
          fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
            | same_name _ _ = false
        in
-         if same_name rtrm qtrm 
-         then rtrm 
+         (* TODO/FIXME: This test is not enough *)
+         if same_name rtrm qtrm then rtrm
          else 
            let 
-             fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)")
-             val exc2   = LIFT_MATCH ("regularize (constant mismatch)")
+             val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)")
+             val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)")
              val thy = ProofContext.theory_of lthy
-             val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) 
+             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
            in 
-             if matches_term (rtrm, rtrm') then rtrm else raise exc2
+             if matches_term (rtrm, rtrm') then rtrm else
+               let
+                 val _ = tracing (Syntax.string_of_term @{context} rtrm);
+                 val _ = tracing (Syntax.string_of_term @{context} rtrm');
+               in raise exc2 end
            end
        end 
 
@@ -616,6 +620,7 @@
   | (_, Const (@{const_name "op ="}, _)) => rtrm
 
     (* FIXME: check here that rtrm is the corresponding definition for the const *)
+    (* Hasn't it already been checked in regularize? *)
   | (_, Const (_, T')) =>
       let
         val rty = fastype_of rtrm

--- a/Quot/quotient_def.ML	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/quotient_def.ML	Wed Dec 09 15:57:47 2009 +0100
@@ -3,10 +3,10 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
-  val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->
+  val make_def: binding -> mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
 
-  val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) ->
+  val quotdef: (binding * term * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * thm) * local_theory
   val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
     local_theory -> local_theory
@@ -79,18 +79,22 @@
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")
 
-fun make_def qconst_bname qty mx attr rhs lthy =
+fun make_def qconst_bname mx attr lhs rhs lthy =
 let
-  val absrep_trm = get_fun absF lthy (fastype_of rhs, qty) $ rhs
-                   |> Syntax.check_term lthy 
+  val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs
+                   |> Syntax.check_term lthy
+  val prop = Logic.mk_equals (lhs, absrep_trm)
+  val (_, prop') = LocalDefs.cert_def lthy prop
+  val (_, newrhs) = Primitive_Defs.abs_def prop'
 
-  val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
+  val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
 
   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
+   val lthy'' = Local_Theory.declaration true
                  (fn phi => 
                        let
-                         val qconst_str = fst (Term.dest_Const (Morphism.term phi trm))
+                         val qconst_str = Binding.name_of qconst_bname
                        in                      
                          qconsts_update_gen qconst_str (qcinfo phi)
                        end) lthy'
@@ -108,27 +112,22 @@
 (* - a meta-equation defining the constant,        *)
 (*   and the attributes of for this meta-equality  *)
 
-fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
-let   
-  val (_, prop') = LocalDefs.cert_def lthy prop
-  val (_, rhs) = Primitive_Defs.abs_def prop'
-in  
-  make_def bind qty mx attr rhs lthy 
-end
+fun quotdef ((bind, lhs, mx), (attr, rhs)) lthy =
+  make_def bind mx attr lhs rhs lthy
 
-fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 
+fun quotdef_cmd ((bind, lhsstr, mx), (attr, rhsstr)) lthy = 
 let
-  val qty  = Syntax.read_typ lthy qtystr
-  val prop = Syntax.read_prop lthy propstr
+  val lhs = Syntax.read_term lthy lhsstr
+  val rhs = Syntax.read_term lthy rhsstr
 in
-  quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
+  quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd
 end
 
 val quotdef_parser =
   (OuterParse.binding --
-    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 
-      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 
-       (SpecParse.opt_thm_name ":" -- OuterParse.prop)
+    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.term --
+      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
+       (SpecParse.opt_thm_name ":" -- OuterParse.term)
 
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)

--- a/Quot/quotient_info.ML	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/quotient_info.ML	Wed Dec 09 15:57:47 2009 +0100
@@ -17,8 +17,8 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
-  val qconsts_lookup: theory -> string -> qconsts_info
-  val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
+  val qconsts_lookup: theory -> term -> qconsts_info
+  val qconsts_update_thy: string -> qconsts_info -> theory -> theory
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
   val qconsts_dest: theory -> qconsts_info list
   val print_qconstinfo: Proof.context -> unit
@@ -145,16 +145,27 @@
      rconst = Morphism.term phi rconst,
      def = Morphism.thm phi def}
 
-fun qconsts_lookup thy str = 
-  case Symtab.lookup (QConstsData.get thy) str of
-    SOME info => info
-  | NONE => raise NotFound
-
-fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
+fun qconsts_update_thy id qcinfo = QConstsData.map (Symtab.update (id, qcinfo))
+fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I
 
 fun qconsts_dest thy =
-    map snd (Symtab.dest (QConstsData.get thy))
+  map snd (Symtab.dest (QConstsData.get thy))
+
+fun qconsts_lookup thy t =
+  let
+    val smt = Symtab.dest (QConstsData.get thy);
+    val (name, qty) = dest_Const t
+    fun matches (_, x) =
+      let
+        val (name', qty') = dest_Const (#qconst x);
+      in
+        name = name' andalso Sign.typ_instance thy (qty, qty')
+      end
+  in
+    case (find_first matches smt) of
+      SOME (_, x) => x
+    | _ => raise NotFound
+  end
 
 (* We don't print the definition *)
 fun print_qconstinfo ctxt =

--- a/isar-keywords-prove.el	Wed Dec 09 06:21:09 2009 +0100
+++ b/isar-keywords-prove.el	Wed Dec 09 15:57:47 2009 +0100
@@ -173,6 +173,7 @@
     "print_locales"
     "print_methods"
     "print_orders"
+    "print_quotconsts"
     "print_quotients"
     "print_rules"
     "print_simpset"
@@ -361,6 +362,7 @@
     "print_locales"
     "print_methods"
     "print_orders"
+    "print_quotconsts"
     "print_quotients"
     "print_rules"
     "print_simpset"