src/Pure/Isar/class.ML
changeset 25518 00d5cc16e891
parent 25514 4b508bb31a6c
child 25536 01753a944433
     1.1 --- a/src/Pure/Isar/class.ML	Mon Dec 03 16:04:14 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Dec 03 16:04:16 2007 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4    val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
     1.5    val conclude_instantiation: local_theory -> local_theory
     1.6  
     1.7 -  val overloaded_const: string * typ * mixfix -> theory -> term * theory
     1.8 +  val overloaded_const: string * typ -> theory -> term * theory
     1.9    val overloaded_def: string -> string * term -> theory -> thm * theory
    1.10    val instantiation_param: Proof.context -> string -> string option
    1.11    val confirm_declaration: string -> local_theory -> local_theory
    1.12 @@ -206,11 +206,8 @@
    1.13    PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
    1.14    #>> (fn [(_, [thm])] => thm);
    1.15  
    1.16 -fun overloaded_const (c, ty, mx) thy =
    1.17 +fun overloaded_const (c, ty) thy =
    1.18    let
    1.19 -    val _ = if mx <> NoSyn then
    1.20 -      error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
    1.21 -      else ();
    1.22      val SOME class = AxClass.class_of_param thy c;
    1.23      val SOME tyco = inst_tyco thy (c, ty);
    1.24      val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
    1.25 @@ -221,7 +218,7 @@
    1.26      |> Sign.sticky_prefix name_inst
    1.27      |> Sign.no_base_names
    1.28      |> Sign.declare_const [] (c', ty', NoSyn)
    1.29 -    |-> (fn const' as Const (c'', _) => Thm.add_def true
    1.30 +    |-> (fn const' as Const (c'', _) => Thm.add_def false true
    1.31            (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
    1.32      #>> Thm.varifyT
    1.33      #-> (fn thm => add_inst (c, tyco) (c'', thm)
    1.34 @@ -241,7 +238,7 @@
    1.35        (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
    1.36    in
    1.37      thy
    1.38 -    |> Thm.add_def false (name', prop)
    1.39 +    |> Thm.add_def false false (name', prop)
    1.40      |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
    1.41    end;
    1.42  
    1.43 @@ -796,7 +793,7 @@
    1.44    in
    1.45      thy'
    1.46      |> Sign.declare_const pos (c, ty'', mx) |> snd
    1.47 -    |> Thm.add_def false (c, def_eq)
    1.48 +    |> Thm.add_def false false (c, def_eq)
    1.49      |>> Thm.symmetric
    1.50      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
    1.51            #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
    1.52 @@ -911,7 +908,6 @@
    1.53      explode #> scan_valids #> implode
    1.54    end;
    1.55  
    1.56 -
    1.57  fun init_instantiation arities thy =
    1.58    let
    1.59      val _ = if null arities then error "At least one arity must be given" else ();
    1.60 @@ -990,7 +986,7 @@
    1.61          |> Sign.sticky_prefix name_inst
    1.62          |> Sign.no_base_names
    1.63          |> Sign.declare_const [] (c', ty, NoSyn)
    1.64 -        |-> (fn const' as Const (c'', _) => Thm.add_def true
    1.65 +        |-> (fn const' as Const (c'', _) => Thm.add_def false true
    1.66                (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
    1.67          #>> Thm.varifyT
    1.68          #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)