Sign.add_consts_authentic: tags (Markup.property list);
authorwenzelm
Sun Sep 30 16:20:31 2007 +0200 (2007-09-30)
changeset 24770695a8e087b9f
parent 24769 1372969969e0
child 24771 6c7e94742afa
Sign.add_consts_authentic: tags (Markup.property list);
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/function_package/size.ML
src/Pure/Isar/class.ML
src/Pure/axclass.ML
src/Pure/pure_thy.ML
src/Tools/code/code_package.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Sep 30 11:55:14 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Sep 30 16:20:31 2007 +0200
     1.3 @@ -320,7 +320,7 @@
     1.4                  fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
     1.5            val ([def_thm], thy') =
     1.6              thy
     1.7 -            |> Sign.add_consts_authentic [decl]
     1.8 +            |> Sign.add_consts_authentic [] [decl]
     1.9              |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
    1.10  
    1.11          in (defs @ [def_thm], thy')
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Sep 30 11:55:14 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Sep 30 16:20:31 2007 +0200
     2.3 @@ -517,7 +517,7 @@
     2.4    end;
     2.5  
     2.6  val specify_consts = gen_specify_consts Sign.add_consts_i;
     2.7 -val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
     2.8 +val specify_consts_authentic = gen_specify_consts (Sign.add_consts_authentic []);
     2.9  
    2.10  structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
    2.11  val interpretation = DatatypeInterpretation.interpretation;
     3.1 --- a/src/HOL/Tools/function_package/size.ML	Sun Sep 30 11:55:14 2007 +0200
     3.2 +++ b/src/HOL/Tools/function_package/size.ML	Sun Sep 30 16:20:31 2007 +0200
     3.3 @@ -31,7 +31,7 @@
     3.4        Const (Sign.full_name thy (Syntax.const_name c mx), T)) args;
     3.5    in
     3.6      thy
     3.7 -    |> Sign.add_consts_authentic args
     3.8 +    |> Sign.add_consts_authentic [] args
     3.9      |> Theory.add_finals_i false specs
    3.10    end;
    3.11  
     4.1 --- a/src/Pure/Isar/class.ML	Sun Sep 30 11:55:14 2007 +0200
     4.2 +++ b/src/Pure/Isar/class.ML	Sun Sep 30 16:20:31 2007 +0200
     4.3 @@ -788,7 +788,7 @@
     4.4    in
     4.5      thy
     4.6      |> Sign.add_path prfx
     4.7 -    |> Sign.add_consts_authentic [(c, ty', syn')]
     4.8 +    |> Sign.add_consts_authentic [] [(c, ty', syn')]
     4.9      |> Sign.parent_path
    4.10      |> Sign.sticky_prefix prfx
    4.11      |> PureThy.add_defs_i false [(def, [])]
     5.1 --- a/src/Pure/axclass.ML	Sun Sep 30 11:55:14 2007 +0200
     5.2 +++ b/src/Pure/axclass.ML	Sun Sep 30 16:20:31 2007 +0200
     5.3 @@ -371,7 +371,7 @@
     5.4      fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
     5.5        (Sign.full_name thy c);
     5.6      fun add_const ((c, ty), syn) =
     5.7 -      Sign.add_consts_authentic [(c, ty, syn)]
     5.8 +      Sign.add_consts_authentic [] [(c, ty, syn)]
     5.9        #> pair (mk_const_name c, ty);
    5.10      fun mk_axioms cs thy =
    5.11        raw_dep_axioms thy cs
     6.1 --- a/src/Pure/pure_thy.ML	Sun Sep 30 11:55:14 2007 +0200
     6.2 +++ b/src/Pure/pure_thy.ML	Sun Sep 30 16:20:31 2007 +0200
     6.3 @@ -499,7 +499,7 @@
     6.4      val def = Logic.mk_equals (list_comb (Const (c, ty), ts), t);
     6.5    in
     6.6      thy
     6.7 -    |> Sign.add_consts_authentic [(raw_c, ty, syn)]
     6.8 +    |> Sign.add_consts_authentic [] [(raw_c, ty, syn)]
     6.9      |> add_defs_i false [((name, def), atts)]
    6.10      |-> (fn [thm] => pair (c, thm))
    6.11    end;
     7.1 --- a/src/Tools/code/code_package.ML	Sun Sep 30 11:55:14 2007 +0200
     7.2 +++ b/src/Tools/code/code_package.ML	Sun Sep 30 16:20:31 2007 +0200
     7.3 @@ -410,8 +410,7 @@
     7.4    let
     7.5      val naming = NameSpace.qualified_names NameSpace.default_naming;
     7.6      val consttab = Consts.empty
     7.7 -      |> fold (fn c => Consts.declare naming
     7.8 -           ((c, CodeFuncgr.typ funcgr c), true))
     7.9 +      |> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c))
    7.10             (CodeFuncgr.all funcgr);
    7.11      val algbr = (Code.operational_algebra thy, consttab);
    7.12    in