src/Pure/axclass.ML
changeset 26516 1bf210ac0a90
parent 26246 e212c22f35c2
child 26939 1035c89b4c02
     1.1 --- a/src/Pure/axclass.ML	Wed Apr 02 15:58:37 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed Apr 02 15:58:38 2008 +0200
     1.3 @@ -258,35 +258,14 @@
     1.4      val prop = Thm.plain_prop_of (Thm.transfer thy th);
     1.5      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
     1.6      val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
     1.7 -    (*FIXME turn this into a mere check as soon as "attach" has disappeared*)
     1.8 -    val missing_params = Sign.complete_sort thy [c]
     1.9 -      |> maps (these o Option.map (fn AxClass { params, ... } => params) o lookup_def thy)
    1.10 -      |> filter_out (fn (p, _) => can (get_inst_param thy) (p, t));
    1.11 -    fun declare_missing (p, T0) thy =
    1.12 -      let
    1.13 -        val name_inst = instance_name (t, c) ^ "_inst";
    1.14 -        val p' = NameSpace.base p ^ "_" ^ NameSpace.base t;
    1.15 -        val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy t) []);
    1.16 -        val T = map_atyps (fn _ => Type (t, map TFree vs)) T0;
    1.17 -      in
    1.18 -        thy
    1.19 -        |> Sign.sticky_prefix name_inst
    1.20 -        |> Sign.no_base_names
    1.21 -        |> Sign.declare_const [] (p', T, NoSyn)
    1.22 -        |-> (fn const' as Const (p'', _) => Thm.add_def false true
    1.23 -              (Thm.def_name p', Logic.mk_equals (const', Const (p, T)))
    1.24 -        #>> Thm.varifyT
    1.25 -        #-> (fn thm => add_inst_param (p, t) (p'', Thm.symmetric thm)
    1.26 -        #> PureThy.note Thm.internalK (p', thm)
    1.27 -        #> snd
    1.28 -        #> Sign.restore_naming thy))
    1.29 -      end;
    1.30 -
    1.31 +    val _ = case filter_out (fn c => can (get_inst_param thy) (c, t)) (params_of thy c)
    1.32 +     of [] => ()
    1.33 +      | cs => Output.legacy_feature
    1.34 +          ("Missing specifications for overloaded parameters " ^ commas_quote cs)
    1.35    in
    1.36      thy
    1.37      |> Sign.primitive_arity (t, Ss, [c])
    1.38      |> put_arity ((t, Ss, c), Drule.unconstrainTs th)
    1.39 -    |> fold declare_missing missing_params
    1.40    end;
    1.41  
    1.42