removed obscure "attach" feature
authorhaftmann
Wed Apr 02 15:58:38 2008 +0200 (2008-04-02 ago)
changeset 265161bf210ac0a90
parent 26515 4a2063a8c2d2
child 26517 ef036a63f6e9
removed obscure "attach" feature
src/Pure/Isar/instance.ML
src/Pure/Isar/isar_syn.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/Isar/instance.ML	Wed Apr 02 15:58:37 2008 +0200
     1.2 +++ b/src/Pure/Isar/instance.ML	Wed Apr 02 15:58:38 2008 +0200
     1.3 @@ -47,18 +47,18 @@
     1.4        in Specification.definition def' ctxt end;
     1.5      val _ = if not (null defs) then Output.legacy_feature
     1.6        "Instance command with attached definitions; use instantiation instead." else ();
     1.7 -  in if not (null defs) orelse forall (Class.is_class thy) sort
     1.8 +  in if null defs
     1.9    then
    1.10      thy
    1.11 +    |> Class.instance_arity I (tyco, map snd vs, sort)
    1.12 +  else
    1.13 +    thy
    1.14      |> TheoryTarget.instantiation ([tyco], vs, sort)
    1.15      |> `(fn ctxt => map (mk_def ctxt) defs)
    1.16      |-> (fn defs => fold_map Specification.definition defs)
    1.17      |> snd
    1.18      |> LocalTheory.restore
    1.19      |> Class.instantiation_instance Class.conclude_instantiation
    1.20 -  else
    1.21 -    thy
    1.22 -    |> Class.instance_arity I (tyco, map snd vs, sort)
    1.23    end;
    1.24  
    1.25  end;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 02 15:58:37 2008 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 02 15:58:38 2008 +0200
     2.3 @@ -433,12 +433,10 @@
     2.4  
     2.5  val _ =
     2.6    OuterSyntax.command "class" "define type class" K.thy_decl
     2.7 -   (P.name --
     2.8 -     Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] --  (* FIXME ?? *)
     2.9 -     (P.$$$ "=" |-- class_val) -- P.opt_begin
    2.10 -    >> (fn (((name, add_consts), (supclasses, elems)), begin) =>
    2.11 +   (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
    2.12 +    >> (fn ((name, (supclasses, elems)), begin) =>
    2.13          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    2.14 -          (Class.class_cmd name supclasses elems add_consts #-> TheoryTarget.begin)));
    2.15 +          (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
    2.16  
    2.17  val _ =
    2.18    OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal
     3.1 --- a/src/Pure/axclass.ML	Wed Apr 02 15:58:37 2008 +0200
     3.2 +++ b/src/Pure/axclass.ML	Wed Apr 02 15:58:38 2008 +0200
     3.3 @@ -258,35 +258,14 @@
     3.4      val prop = Thm.plain_prop_of (Thm.transfer thy th);
     3.5      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
     3.6      val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
     3.7 -    (*FIXME turn this into a mere check as soon as "attach" has disappeared*)
     3.8 -    val missing_params = Sign.complete_sort thy [c]
     3.9 -      |> maps (these o Option.map (fn AxClass { params, ... } => params) o lookup_def thy)
    3.10 -      |> filter_out (fn (p, _) => can (get_inst_param thy) (p, t));
    3.11 -    fun declare_missing (p, T0) thy =
    3.12 -      let
    3.13 -        val name_inst = instance_name (t, c) ^ "_inst";
    3.14 -        val p' = NameSpace.base p ^ "_" ^ NameSpace.base t;
    3.15 -        val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy t) []);
    3.16 -        val T = map_atyps (fn _ => Type (t, map TFree vs)) T0;
    3.17 -      in
    3.18 -        thy
    3.19 -        |> Sign.sticky_prefix name_inst
    3.20 -        |> Sign.no_base_names
    3.21 -        |> Sign.declare_const [] (p', T, NoSyn)
    3.22 -        |-> (fn const' as Const (p'', _) => Thm.add_def false true
    3.23 -              (Thm.def_name p', Logic.mk_equals (const', Const (p, T)))
    3.24 -        #>> Thm.varifyT
    3.25 -        #-> (fn thm => add_inst_param (p, t) (p'', Thm.symmetric thm)
    3.26 -        #> PureThy.note Thm.internalK (p', thm)
    3.27 -        #> snd
    3.28 -        #> Sign.restore_naming thy))
    3.29 -      end;
    3.30 -
    3.31 +    val _ = case filter_out (fn c => can (get_inst_param thy) (c, t)) (params_of thy c)
    3.32 +     of [] => ()
    3.33 +      | cs => Output.legacy_feature
    3.34 +          ("Missing specifications for overloaded parameters " ^ commas_quote cs)
    3.35    in
    3.36      thy
    3.37      |> Sign.primitive_arity (t, Ss, [c])
    3.38      |> put_arity ((t, Ss, c), Drule.unconstrainTs th)
    3.39 -    |> fold declare_missing missing_params
    3.40    end;
    3.41  
    3.42