# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256755575 -3600
# Node ID 84a356e3d38bed2d78ea383fb82050dd4dd07f36
# Parent  13f985a93dbc478ef9a501d98fd3ffeeb511408a
ported all constant definitions to new scheme

diff -r 13f985a93dbc -r 84a356e3d38b QuotTest.thy
--- a/QuotTest.thy	Wed Oct 28 19:36:52 2009 +0100
+++ b/QuotTest.thy	Wed Oct 28 19:46:15 2009 +0100
@@ -81,21 +81,21 @@
 *}
 
 ML {*
-  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
+  get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
-  get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
+  get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
-  get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+  get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
   |> fst
   |> Syntax.pretty_term @{context}
   |> Pretty.string_of
@@ -111,11 +111,20 @@
 *}
 *)
 
-local_setup {*
-  make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
-  make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
-  make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
-*}
+quotient_def (for qt)
+  VR ::"string \<Rightarrow> qt"
+where
+  "VR \<equiv> vr"
+
+quotient_def (for qt)
+  AP ::"qt list \<Rightarrow> qt"
+where
+  "AP \<equiv> ap"
+
+quotient_def (for qt)
+  LM ::"string \<Rightarrow> qt \<Rightarrow> qt"
+where
+  "LM \<equiv> lm"
 
 term vr
 term ap
@@ -141,11 +150,21 @@
 print_quotients
 print_theorems
 
-local_setup {*
-  make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
-  make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
-  make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
-*}
+
+quotient_def (for "'a qt'")
+  VR' ::"string \<Rightarrow> 'a qt"
+where
+  "VR' \<equiv> vr'"
+
+quotient_def (for "'a qt'")
+  AP' ::"('a qt') * ('a qt') \<Rightarrow> 'a qt"
+where
+  "AP' \<equiv> ap'"
+
+quotient_def (for "'a qt'")
+  LM' ::"'a \<Rightarrow> string \<Rightarrow> 'a qt'"
+where
+  "LM' \<equiv> lm'"
 
 term vr'
 term ap'