--- a/Quot/Examples/FSet.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/FSet.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -27,18 +27,18 @@
   done
 
 quotient_def
-  EMPTY :: "EMPTY :: 'a fset"
-where
+   "EMPTY :: 'a fset"
+as
   "[]::'a list"
 
 quotient_def
-  INSERT :: "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+   "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
   "op #"
 
 quotient_def
-  FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+   "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
   "op @"
 
 fun
@@ -48,8 +48,8 @@
 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
 
 quotient_def
-  CARD :: "CARD :: 'a fset \<Rightarrow> nat"
-where
+   "CARD :: 'a fset \<Rightarrow> nat"
+as
   "card1"
 
 (* text {*
@@ -111,18 +111,18 @@
   done
 
 quotient_def
-  IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-where
+   "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+as
   "op mem"
 
 quotient_def
-  FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+   "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
   "fold1"
 
 quotient_def
-  fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-where
+  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+as
   "map"
 
 lemma mem_rsp:
@@ -275,13 +275,13 @@
   by (rule equivp_list_eq)
 
 quotient_def
-  EMPTY2 :: "EMPTY2 :: 'a fset2"
-where
+   "EMPTY2 :: 'a fset2"
+as
   "[]::'a list"
 
 quotient_def
-  INSERT2 :: "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
-where
+   "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+as
   "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"
@@ -293,13 +293,13 @@
 done
 
 quotient_def
-  fset_rec::"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+  "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
   "list_rec"
 
 quotient_def
-  fset_case::"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
   "list_case"
 
 (* Probably not true without additional assumptions about the function *)

--- a/Quot/Examples/FSet2.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/FSet2.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -24,23 +24,23 @@
 quotient fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def 
-  fempty :: "fempty :: 'a fset" ("{||}")
-where
+quotient_def
+  "fempty :: 'a fset" ("{||}")
+as
   "[]"
 
-quotient_def 
-  finsert :: "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+quotient_def
+  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
   "(op #)"
 
 lemma finsert_rsp[quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
 by (auto intro: list_eq.intros)
 
-quotient_def 
-  funion :: "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
-where
+quotient_def
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
+as
   "(op @)"
 
 lemma append_rsp_aux1:
@@ -65,9 +65,9 @@
   by (auto simp add: append_rsp_aux2)
 
 
-quotient_def 
-  fmem :: " fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
-where
+quotient_def
+  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+as
   "(op mem)"
 
 lemma memb_rsp_aux:
@@ -89,9 +89,9 @@
 where
   "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
 
-quotient_def 
-  finter :: "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
-where
+quotient_def
+  "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+as
   "inter_list"
 
 no_syntax

--- a/Quot/Examples/IntEx.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -22,13 +22,13 @@
 print_quotients
 
 quotient_def
-  ZERO::"zero :: my_int"
-where
+  "ZERO :: my_int"
+as
   "(0::nat, 0::nat)"
 
 quotient_def
-  ONE::"one :: my_int"
-where
+  "ONE :: my_int"
+as
   "(1::nat, 0::nat)"
 
 fun
@@ -37,8 +37,8 @@
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
 quotient_def
-  PLUS::"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
+  "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+as
   "my_plus"
 
 fun
@@ -47,8 +47,8 @@
   "my_neg (x, y) = (y, x)"
 
 quotient_def
-  NEG::"NEG :: my_int \<Rightarrow> my_int"
-where
+  "NEG :: my_int \<Rightarrow> my_int"
+as
   "my_neg"
 
 definition
@@ -62,8 +62,8 @@
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_def
-  MULT::"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
+  "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
+as
   "my_mult"
 
 
@@ -74,8 +74,8 @@
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_def
-  LE :: "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
-where
+   "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
+as
   "my_le"
 
 term LE

--- a/Quot/Examples/IntEx2.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -18,15 +18,13 @@
 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
 begin
 
-quotient_def
-  zero_int::"0 :: int"
-where
-  "(0::nat, 0::nat)"
+ML {* @{term "0 :: int"} *}
 
 quotient_def
-  one_int::"1 :: int"
-where
-  "(1::nat, 0::nat)"
+  "0 :: int" as "(0::nat, 0::nat)"
+
+quotient_def
+  "1 :: int" as "(1::nat, 0::nat)"
 
 fun
   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -34,9 +32,7 @@
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
 quotient_def
-  plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)"
-where
-  "plus_raw"
+  "(op +) :: (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
 
 fun
   uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -44,9 +40,7 @@
   "uminus_raw (x, y) = (y, x)"
 
 quotient_def
-  uminus_int::"(uminus :: (int \<Rightarrow> int))"
-where
-  "uminus_raw"
+  "(uminus :: (int \<Rightarrow> int))" as "uminus_raw"
 
 definition
   minus_int_def [code del]:  "z - w = z + (-w::int)"
@@ -57,9 +51,7 @@
   "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_def
-  times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)"
-where
-  "times_raw"
+  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "times_raw"
 
 (* PROBLEM: this should be called le_int and le_raw / or odd *)
 fun
@@ -68,9 +60,7 @@
   "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_def
-  less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
-where
-  "less_eq_raw"
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "less_eq_raw"
 
 definition
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -218,8 +208,7 @@
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
 quotient_def
-  int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" 
-where "int_of_nat_raw"
+  "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
 
 lemma[quot_respect]: 
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"

--- a/Quot/Examples/LFex.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/LFex.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -81,49 +81,49 @@
   by (auto intro: alpha_equivps)
 
 quotient_def
-  TYP :: "TYP :: KIND"
-where
+   "TYP :: KIND"
+as
   "Type"
 
 quotient_def
-  KPI :: "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
-where
+   "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
+as
   "KPi"
 
 quotient_def
-  TCONST :: "TCONST :: ident \<Rightarrow> TY"
-where
+   "TCONST :: ident \<Rightarrow> TY"
+as
   "TConst"
 
 quotient_def
-  TAPP :: "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
-where
+   "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
+as
   "TApp"
 
 quotient_def
-  TPI :: "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
-where
+   "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
+as
   "TPi"
 
 (* FIXME: does not work with CONST *)
 quotient_def
-  CONS :: "CONS :: ident \<Rightarrow> TRM"
-where
+   "CONS :: ident \<Rightarrow> TRM"
+as
   "Const"
 
 quotient_def
-  VAR :: "VAR :: name \<Rightarrow> TRM"
-where
+   "VAR :: name \<Rightarrow> TRM"
+as
   "Var"
 
 quotient_def
-  APP :: "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+   "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
+as
   "App"
 
 quotient_def
-  LAM :: "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+   "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
+as
   "Lam"
 
 thm TYP_def
@@ -138,18 +138,18 @@
 
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
 quotient_def
-  FV_kind :: "FV_kind :: KIND \<Rightarrow> name set"
-where
+   "FV_kind :: KIND \<Rightarrow> name set"
+as
   "fv_kind"
 
 quotient_def
-  FV_ty :: "FV_ty :: TY \<Rightarrow> name set"
-where
+   "FV_ty :: TY \<Rightarrow> name set"
+as
   "fv_ty"
 
 quotient_def
-  FV_trm :: "FV_trm :: TRM \<Rightarrow> name set"
-where
+   "FV_trm :: TRM \<Rightarrow> name set"
+as
   "fv_trm"
 
 thm FV_kind_def
@@ -164,18 +164,18 @@
 begin
 
 quotient_def
-  perm_kind :: "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
-where
+   "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
+as
   "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
 
 quotient_def
-  perm_ty :: "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
-where
+   "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
+as
   "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
 
 quotient_def
-  perm_trm :: "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
-where
+   "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
+as
   "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 end

--- a/Quot/Examples/LamEx.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -57,18 +57,18 @@
 print_quotients
 
 quotient_def
-  Var :: "Var :: name \<Rightarrow> lam"
-where
+   "Var :: name \<Rightarrow> lam"
+as
   "rVar"
 
 quotient_def
-  App :: "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-where
+   "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
+as
   "rApp"
 
 quotient_def
-  Lam :: "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-where
+   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
+as
   "rLam"
 
 thm Var_def
@@ -76,8 +76,8 @@
 thm Lam_def
 
 quotient_def
-  fv :: "fv :: lam \<Rightarrow> name set"
-where
+   "fv :: lam \<Rightarrow> name set"
+as
   "rfv"
 
 thm fv_def
@@ -89,18 +89,12 @@
 begin
 
 quotient_def
-  perm_lam :: "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
-where
+   "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
+as
   "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 end
 
-(*quotient_def (for lam)
-  abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
-where
-  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"*)
-
-
 thm perm_lam_def
 
 (* lemmas that need to lift *)

--- a/Quot/Examples/Larry.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/Larry.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -128,23 +128,23 @@
 text{*The abstract message constructors*}
 
 quotient_def
-  Nonce::"Nonce :: nat \<Rightarrow> msg"
-where
+  "Nonce :: nat \<Rightarrow> msg"
+as
   "NONCE"
 
 quotient_def
-  MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-where
+  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+as
   "MPAIR"
 
 quotient_def
-  Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
+  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+as
   "CRYPT"
 
 quotient_def
-  Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
+  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+as
   "DECRYPT"
 
 lemma [quot_respect]:
@@ -165,8 +165,8 @@
 subsection{*The Abstract Function to Return the Set of Nonces*}
 
 quotient_def
-  nonces :: "nounces:: msg \<Rightarrow> nat set"
-where
+   "nonces:: msg \<Rightarrow> nat set"
+as
   "freenonces"
 
 text{*Now prove the four equations for @{term nonces}*}
@@ -201,8 +201,8 @@
 subsection{*The Abstract Function to Return the Left Part*}
 
 quotient_def
-  left :: "left:: msg \<Rightarrow> msg"
-where
+  "left:: msg \<Rightarrow> msg"
+as
   "freeleft"
 
 lemma [quot_respect]:
@@ -228,8 +228,8 @@
 subsection{*The Abstract Function to Return the Right Part*}
 
 quotient_def
-  right :: "right:: msg \<Rightarrow> msg"
-where
+  "right:: msg \<Rightarrow> msg"
+as
   "freeright"
 
 text{*Now prove the four equations for @{term right}*}
@@ -362,8 +362,8 @@
 need this function in order to prove discrimination theorems.*}
 
 quotient_def
-  discrim :: "discrim:: msg \<Rightarrow> int"
-where
+  "discrim:: msg \<Rightarrow> int"
+as
   "freediscrim"
 
 text{*Now prove the four equations for @{term discrim}*}

--- a/Quot/quotient_def.ML	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 11 11:08:58 2009 +0100
@@ -3,12 +3,9 @@
 sig
   datatype flag = absF | repF
   val get_fun: flag -> Proof.context -> typ * typ -> term
-  val make_def: binding -> mixfix -> Attrib.binding -> term -> term ->
+  val make_def: mixfix -> Attrib.binding -> term -> term ->
     Proof.context -> (term * thm) * local_theory
-
-  val quotdef: (binding * term * mixfix) * (Attrib.binding * term) ->
-    local_theory -> (term * thm) * local_theory
-  val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
+  val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
 end;
 
@@ -79,9 +76,11 @@
   | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
   | _ => raise (LIFT_MATCH "get_fun")
 
-fun make_def qconst_bname mx attr lhs rhs lthy =
+fun make_def mx attr lhs rhs lthy =
 let
-  val absrep_trm = get_fun absF lthy (fastype_of rhs, fastype_of lhs) $ rhs
+  val Free (lhs_str, lhs_ty) = lhs;
+  val qconst_bname = Binding.name lhs_str;
+  val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
                    |> Syntax.check_term lthy
   val prop = Logic.mk_equals (lhs, absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
@@ -91,12 +90,7 @@
 
   fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => 
-                       let
-                         val qconst_str = Binding.name_of qconst_bname
-                       in                      
-                         qconsts_update_gen qconst_str (qcinfo phi)
-                       end) lthy'
+                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end
@@ -111,22 +105,21 @@
 (* - a meta-equation defining the constant,        *)
 (*   and the attributes of for this meta-equality  *)
 
-fun quotdef ((bind, lhs, mx), (attr, rhs)) lthy =
-  make_def bind mx attr lhs rhs lthy
-
-fun quotdef_cmd ((bind, lhsstr, mx), (attr, rhsstr)) lthy = 
+fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = 
 let
   val lhs = Syntax.read_term lthy lhsstr
   val rhs = Syntax.read_term lthy rhsstr
 in
-  quotdef ((bind, lhs, mx), (attr, rhs)) lthy |> snd
+  make_def mx attr lhs rhs lthy |> snd
 end
 
+val _ = OuterKeyword.keyword "as";
+
 val quotdef_parser =
-  (OuterParse.binding --
-    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.term --
-      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
-       (SpecParse.opt_thm_name ":" -- OuterParse.term)
+  (SpecParse.opt_thm_name ":" --
+  OuterParse.term) --
+  (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
+  OuterParse.term)
 
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)

--- a/isar-keywords-prove.el	Fri Dec 11 08:28:41 2009 +0100
+++ b/isar-keywords-prove.el	Fri Dec 11 11:08:58 2009 +0100
@@ -257,6 +257,7 @@
 (defconst isar-keywords-minor
   '("advanced"
     "and"
+    "as"
     "assumes"
     "attach"
     "avoids"