src/Pure/axclass.ML
changeset 35201 c2ddb9395436
parent 35021 c839a4c670c6
child 35238 18ae6ef02fe0
     1.1 --- a/src/Pure/axclass.ML	Thu Feb 18 20:46:46 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Feb 18 21:26:40 2010 +0100
     1.3 @@ -286,23 +286,25 @@
     1.4  
     1.5  (* declaration and definition of instances of overloaded constants *)
     1.6  
     1.7 -fun inst_tyco_of thy (c, T) = case get_inst_tyco (Sign.consts_of thy) (c, T)
     1.8 - of SOME tyco => tyco
     1.9 -  | NONE => error ("Illegal type for instantiation of class parameter: "
    1.10 -      ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
    1.11 +fun inst_tyco_of thy (c, T) =
    1.12 +  (case get_inst_tyco (Sign.consts_of thy) (c, T) of
    1.13 +    SOME tyco => tyco
    1.14 +  | NONE => error ("Illegal type for instantiation of class parameter: " ^
    1.15 +      quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T)));
    1.16  
    1.17  fun declare_overloaded (c, T) thy =
    1.18    let
    1.19 -    val class = case class_of_param thy c
    1.20 -     of SOME class => class
    1.21 -      | NONE => error ("Not a class parameter: " ^ quote c);
    1.22 +    val class =
    1.23 +      (case class_of_param thy c of
    1.24 +        SOME class => class
    1.25 +      | NONE => error ("Not a class parameter: " ^ quote c));
    1.26      val tyco = inst_tyco_of thy (c, T);
    1.27      val name_inst = instance_name (tyco, class) ^ "_inst";
    1.28      val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
    1.29      val T' = Type.strip_sorts T;
    1.30    in
    1.31      thy
    1.32 -    |> Sign.mandatory_path name_inst
    1.33 +    |> Sign.qualified_path true (Binding.name name_inst)
    1.34      |> Sign.declare_const ((Binding.name c', T'), NoSyn)
    1.35      |-> (fn const' as Const (c'', _) =>
    1.36        Thm.add_def false true
    1.37 @@ -311,8 +313,8 @@
    1.38        #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
    1.39        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    1.40        #> snd
    1.41 -      #> Sign.restore_naming thy
    1.42        #> pair (Const (c, T))))
    1.43 +    ||> Sign.restore_naming thy
    1.44    end;
    1.45  
    1.46  fun define_overloaded b (c, t) thy =
    1.47 @@ -482,7 +484,7 @@
    1.48      val class_triv = Thm.class_triv def_thy class;
    1.49      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
    1.50        def_thy
    1.51 -      |> Sign.mandatory_path (Binding.name_of bconst)
    1.52 +      |> Sign.qualified_path true bconst
    1.53        |> PureThy.note_thmss ""
    1.54          [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
    1.55           ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
    1.56 @@ -497,7 +499,7 @@
    1.57      val result_thy =
    1.58        facts_thy
    1.59        |> fold put_classrel (map (pair class) super ~~ classrel)
    1.60 -      |> Sign.add_path (Binding.name_of bconst)
    1.61 +      |> Sign.qualified_path false bconst
    1.62        |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
    1.63        |> Sign.restore_naming facts_thy
    1.64        |> map_axclasses (fn (axclasses, parameters) =>