1.1 --- a/src/Pure/Isar/code.ML	Fri Nov 26 23:49:49 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Fri Nov 26 23:49:49 2010 +0100
     1.3 @@ -316,7 +316,7 @@
     1.4      val data = case Datatab.lookup datatab kind
     1.5       of SOME data => data
     1.6        | NONE => invoke_init kind;
     1.7 -    val result as (x, data') = f (dest data);
     1.8 +    val result as (_, data') = f (dest data);
     1.9      val _ = Synchronized.change dataref
    1.10        ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
    1.11    in result end;
    1.12 @@ -360,9 +360,9 @@
    1.13  
    1.14  fun subst_signature thy c ty =
    1.15    let
    1.16 -    fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
    1.17 +    fun mk_subst (Type (_, tys1)) (Type (_, tys2)) =
    1.18            fold2 mk_subst tys1 tys2
    1.19 -      | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
    1.20 +      | mk_subst ty (TVar (v, _)) = Vartab.update (v, ([], ty))
    1.21    in case lookup_typ thy c
    1.22     of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
    1.23      | NONE => ty
    1.24 @@ -407,8 +407,9 @@
    1.25          val _ = if (tyco' : string) <> tyco
    1.26            then error "Different type constructors in constructor set"
    1.27            else ();
    1.28 -        val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
    1.29 -      in ((tyco, sorts), c :: cs) end;
    1.30 +        val sorts'' =
    1.31 +          map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
    1.32 +      in ((tyco, sorts''), c :: cs) end;
    1.33      fun inst vs' (c, (vs, ty)) =
    1.34        let
    1.35          val the_v = the o AList.lookup (op =) (vs ~~ vs');
    1.36 @@ -439,7 +440,7 @@
    1.37   
    1.38  fun get_type_of_constr_or_abstr thy c =
    1.39    case (snd o strip_type o const_typ thy) c
    1.40 -   of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
    1.41 +   of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
    1.42          in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
    1.43      | _ => NONE;
    1.44  
    1.45 @@ -641,19 +642,19 @@
    1.46      else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
    1.47    end;
    1.48  
    1.49 -fun desymbolize_tvars thy thms =
    1.50 +fun desymbolize_tvars thms =
    1.51    let
    1.52      val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
    1.53      val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
    1.54    in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
    1.55  
    1.56 -fun desymbolize_vars thy thm =
    1.57 +fun desymbolize_vars thm =
    1.58    let
    1.59      val vs = Term.add_vars (Thm.prop_of thm) [];
    1.60      val var_subst = mk_desymbolization I I Var vs;
    1.61    in Thm.certify_instantiate ([], var_subst) thm end;
    1.62  
    1.63 -fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
    1.64 +fun canonize_thms thy = desymbolize_tvars #> same_arity thy #> map desymbolize_vars;
    1.65  
    1.66  
    1.67  (* abstype certificates *)
    1.68 @@ -672,13 +673,12 @@
    1.69        then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
    1.70      val _ = check_decl_ty thy (abs, raw_ty);
    1.71      val _ = check_decl_ty thy (rep, rep_ty);
    1.72 -    val var = (fst o dest_Var) param
    1.73 +    val _ = (fst o dest_Var) param
    1.74        handle TERM _ => bad "Not an abstype certificate";
    1.75      val _ = if param = rhs then () else bad "Not an abstype certificate";
    1.76      val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
    1.77      val ty = domain_type ty';
    1.78      val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
    1.79 -    val ty_abs = range_type ty';
    1.80    in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
    1.81  
    1.82  
    1.83 @@ -716,7 +716,7 @@
    1.84  
    1.85  fun concretify_abs thy tyco abs_thm =
    1.86    let
    1.87 -    val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
    1.88 +    val (_, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
    1.89      val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
    1.90      val ty = fastype_of lhs;
    1.91      val ty_abs = (fastype_of o snd o dest_comb) lhs;
    1.92 @@ -746,8 +746,11 @@
    1.93      val tvars = Term.add_tvar_namesT raw_ty [];
    1.94      val tvars' = case AxClass.class_of_param thy c
    1.95       of SOME class => [TFree (Name.aT, [class])]
    1.96 -      | NONE => Name.invent_list [] Name.aT (length tvars)
    1.97 -          |> map (fn v => TFree (v, []));
    1.98 +      | NONE =>  (case get_type_of_constr_or_abstr thy c
    1.99 +         of SOME (tyco, _) => map TFree ((fst o the)
   1.100 +              (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c))
   1.101 +          | NONE => Name.invent_list [] Name.aT (length tvars)
   1.102 +              |> map (fn v => TFree (v, [])));
   1.103      val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
   1.104      val chead = build_head thy (c, ty);
   1.105    in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
   1.106 @@ -767,19 +770,19 @@
   1.107            fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
   1.108          val sorts = map_transpose inter_sorts vss;
   1.109          val vts = Name.names Name.context Name.aT sorts;
   1.110 -        val thms as thm :: _ =
   1.111 +        val thms' =
   1.112            map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
   1.113 -        val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms))));
   1.114 +        val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
   1.115          fun head_conv ct = if can Thm.dest_comb ct
   1.116            then Conv.fun_conv head_conv ct
   1.117            else Conv.rewr_conv head_thm ct;
   1.118          val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
   1.119 -        val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
   1.120 +        val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
   1.121        in Equations (cert_thm, propers) end;
   1.122  
   1.123  fun cert_of_proj thy c tyco =
   1.124    let
   1.125 -    val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
   1.126 +    val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
   1.127      val _ = if c = rep then () else
   1.128        error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
   1.129    in Projection (mk_proj tyco vs ty abs rep, tyco) end;
   1.130 @@ -824,7 +827,7 @@
   1.131            Thm.prop_of cert_thm
   1.132            |> Logic.dest_conjunction_balanced (length propers);
   1.133        in (vs, fold (add_rhss_of_eqn thy) equations []) end
   1.134 -  | typargs_deps_of_cert thy (Projection (t, tyco)) =
   1.135 +  | typargs_deps_of_cert thy (Projection (t, _)) =
   1.136        (fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
   1.137    | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
   1.138        let
   1.139 @@ -864,7 +867,7 @@
   1.140           o snd o equations_of_cert thy) cert
   1.141    | pretty_cert thy (Projection (t, _)) =
   1.142        [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
   1.143 -  | pretty_cert thy (Abstract (abs_thm, tyco)) =
   1.144 +  | pretty_cert thy (Abstract (abs_thm, _)) =
   1.145        [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
   1.146  
   1.147  fun bare_thms_of_cert thy (cert as Equations _) =
   1.148 @@ -1118,7 +1121,7 @@
   1.149  
   1.150  fun del_eqn thm thy = case mk_eqn_liberal thy thm
   1.151   of SOME (thm, _) => let
   1.152 -        fun del_eqn' (Default eqns) = empty_fun_spec
   1.153 +        fun del_eqn' (Default _) = empty_fun_spec
   1.154            | del_eqn' (Eqns eqns) =
   1.155                Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
   1.156            | del_eqn' spec = spec
   1.157 @@ -1130,7 +1133,7 @@
   1.158  
   1.159  (* cases *)
   1.160  
   1.161 -fun case_cong thy case_const (num_args, (pos, constrs)) =
   1.162 +fun case_cong thy case_const (num_args, (pos, _)) =
   1.163    let
   1.164      val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
   1.165      val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;