merged

--- a/src/HOL/HOL.thy	Wed Feb 18 17:02:00 2009 -0800
+++ b/src/HOL/HOL.thy	Wed Feb 18 17:02:38 2009 -0800
@@ -290,7 +290,7 @@
 typed_print_translation {*
 let
   fun tr' c = (c, fn show_sorts => fn T => fn ts =>
-    if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
+    if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
 in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
 *} -- {* show types that are presumably too general *}

--- a/src/Pure/Isar/class_target.ML	Wed Feb 18 17:02:00 2009 -0800
+++ b/src/Pure/Isar/class_target.ML	Wed Feb 18 17:02:38 2009 -0800
@@ -493,7 +493,7 @@
 fun init_instantiation (tycos, vs, sort) thy =
   let
     val _ = if null tycos then error "At least one arity must be given" else ();
-    val params = these_params thy sort;
+    val params = these_params thy (filter (can (AxClass.get_info thy)) sort);
     fun get_param tyco (param, (_, (c, ty))) =
       if can (AxClass.param_of_inst thy) (c, tyco)
       then NONE else SOME ((c, tyco),
@@ -513,7 +513,8 @@
       | SOME ts' => SOME (ts', ctxt);
     fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
-         of SOME (_, ty') => if Type.raw_instance (ty', ty) then SOME (ty, ty') else NONE
+         of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
+              then SOME (ty, ty') else NONE
           | NONE => NONE)
       | NONE => NONE;
   in
@@ -523,8 +524,7 @@
     |> fold (Variable.declare_typ o TFree) vs
     |> fold (Variable.declare_names o Free o snd) inst_params
     |> (Overloading.map_improvable_syntax o apfst)
-         (fn ((_, _), ((_, subst), unchecks)) =>
-            ((primary_constraints, []), (((improve, K NONE), false), [])))
+         (K ((primary_constraints, []), (((improve, K NONE), false), [])))
     |> Overloading.add_improvable_syntax
     |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax

--- a/src/Pure/Isar/code.ML	Wed Feb 18 17:02:00 2009 -0800
+++ b/src/Pure/Isar/code.ML	Wed Feb 18 17:02:38 2009 -0800
@@ -35,7 +35,7 @@
   val these_raw_eqns: theory -> string -> (thm * bool) list
   val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
   val get_datatype_of_constr: theory -> string -> string option
-  val get_case_data: theory -> string -> (int * string list) option
+  val get_case_scheme: theory -> string -> (int * string list) option
   val is_undefined: theory -> string -> bool
   val default_typscheme: theory -> string -> (string * sort) list * typ
 
@@ -583,7 +583,7 @@
 
 fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
 
-val get_case_data = Symtab.lookup o fst o the_cases o the_exec;
+fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
 
 val is_undefined = Symtab.defined o snd o the_cases o the_exec;
 

--- a/src/Pure/Isar/theory_target.ML	Wed Feb 18 17:02:00 2009 -0800
+++ b/src/Pure/Isar/theory_target.ML	Wed Feb 18 17:02:38 2009 -0800
@@ -13,7 +13,7 @@
   val begin: string -> Proof.context -> local_theory
   val context: xstring -> theory -> local_theory
   val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
-  val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
+  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
   val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
   val overloading_cmd: (string * string * bool) list -> theory -> local_theory
 end;

--- a/src/Pure/sorts.ML	Wed Feb 18 17:02:00 2009 -0800
+++ b/src/Pure/sorts.ML	Wed Feb 18 17:02:38 2009 -0800
@@ -302,11 +302,21 @@
 
 (* algebra projections *)
 
-fun classrels_of (Algebra {classes, ...}) =
-  map (fn [c] => (c, Graph.imm_succs classes c)) (rev (Graph.strong_conn classes));
+val sorted_classes = rev o flat o Graph.strong_conn o classes_of;
+
+fun classrels_of algebra = 
+  map (fn c => (c, Graph.imm_succs (classes_of algebra) c)) (sorted_classes algebra);
 
-fun instances_of (Algebra {arities, ...}) =
-  Symtab.fold (fn (a, cs) => append (map (pair a o fst) cs)) arities [];
+fun instances_of algebra =
+  let
+    val arities = arities_of algebra;
+    val all_classes = sorted_classes algebra;
+    fun sort_classes cs = filter (member (op = o apsnd fst) cs)
+      all_classes;
+  in
+    Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
+      arities []
+  end;
 
 fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   let

--- a/src/Tools/code/code_funcgr_new.ML	Wed Feb 18 17:02:00 2009 -0800
+++ b/src/Tools/code/code_funcgr_new.ML	Wed Feb 18 17:02:38 2009 -0800
@@ -205,16 +205,6 @@
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
   end;
 
-fun instances_of (*FIXME move to sorts.ML*) algebra =
-  let
-    val { classes, arities } = Sorts.rep_algebra algebra;
-    val sort_classes = fn cs => filter (member (op = o apsnd fst) cs)
-      (flat (rev (Graph.strong_conn classes)));
-  in
-    Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
-      arities []
-  end;
-
 fun algebra_of thy vardeps =
   let
     val pp = Syntax.pp_global thy;
@@ -223,7 +213,7 @@
     val classrels = Sorts.classrels_of thy_algebra
       |> filter (is_proper o fst)
       |> (map o apsnd) (filter is_proper);
-    val instances = instances_of thy_algebra
+    val instances = Sorts.instances_of thy_algebra
       |> filter (is_proper o snd);
     fun add_class (class, superclasses) algebra =
       Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;

--- a/src/Tools/code/code_thingol.ML	Wed Feb 18 17:02:00 2009 -0800
+++ b/src/Tools/code/code_thingol.ML	Wed Feb 18 17:02:38 2009 -0800
@@ -461,12 +461,6 @@
 
 (* translation *)
 
-(*FIXME move to code(_unit).ML*)
-fun get_case_scheme thy c = case Code.get_case_data thy c
- of SOME (proto_case_scheme as (_, case_pats)) => 
-      SOME (1 + (if null case_pats then 1 else length case_pats), proto_case_scheme)
-  | NONE => NONE
-
 fun ensure_class thy (algbr as (_, algebra)) funcgr class =
   let
     val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -638,7 +632,7 @@
     ##>> fold_map (translate_typ thy algbr funcgr) tys_args
     #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
   end
-and translate_app_default thy algbr funcgr thm (c_ty, ts) =
+and translate_app_const thy algbr funcgr thm (c_ty, ts) =
   translate_const thy algbr funcgr thm c_ty
   ##>> fold_map (translate_term thy algbr funcgr thm) ts
   #>> (fn (t, ts) => t `$$ ts)
@@ -689,26 +683,30 @@
       #>> pair b) clauses
     #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
   end
-and translate_app thy algbr funcgr thm ((c, ty), ts) = case get_case_scheme thy c
- of SOME (case_scheme as (num_args, _)) =>
-      if length ts < num_args then
-        let
-          val k = length ts;
-          val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
-          val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
-          val vs = Name.names ctxt "a" tys;
-        in
-          fold_map (translate_typ thy algbr funcgr) tys
-          ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
-          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
-        end
-      else if length ts > num_args then
-        translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
-        ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
-        #>> (fn (t, ts) => t `$$ ts)
-      else
-        translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
-  | NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);
+and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
+  if length ts < num_args then
+    let
+      val k = length ts;
+      val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
+      val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
+      val vs = Name.names ctxt "a" tys;
+    in
+      fold_map (translate_typ thy algbr funcgr) tys
+      ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
+      #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
+    end
+  else if length ts > num_args then
+    translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
+    ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
+    #>> (fn (t, ts) => t `$$ ts)
+  else
+    translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
+and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
+  case Code.get_case_scheme thy c
+   of SOME (base_case_scheme as (_, case_pats)) =>
+        translate_app_case thy algbr funcgr thm
+          (1 + Int.max (1, length case_pats), base_case_scheme) c_ty_ts
+    | NONE => translate_app_const thy algbr funcgr thm c_ty_ts;
 
 
 (* store *)