src/Pure/facts.ML
changeset 28965 1de908189869
parent 28941 128459bd72d2
child 29269 5c25a2012975
equal deleted inserted replaced
28963:f6d9e0e0b153 28965:1de908189869
    29   val dest_static: T list -> T -> (string * thm list) list
    29   val dest_static: T list -> T -> (string * thm list) list
    30   val extern_static: T list -> T -> (xstring * thm list) list
    30   val extern_static: T list -> T -> (xstring * thm list) list
    31   val props: T -> thm list
    31   val props: T -> thm list
    32   val could_unify: T -> term -> thm list
    32   val could_unify: T -> term -> thm list
    33   val merge: T * T -> T
    33   val merge: T * T -> T
    34   val add_global: NameSpace.naming -> Name.binding * thm list -> T -> string * T
    34   val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
    35   val add_local: bool -> NameSpace.naming -> Name.binding * thm list -> T -> string * T
    35   val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
    36   val add_dynamic: NameSpace.naming -> Name.binding * (Context.generic -> thm list) -> T -> string * T
    36   val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
    37   val del: string -> T -> T
    37   val del: string -> T -> T
    38   val hide: bool -> string -> T -> T
    38   val hide: bool -> string -> T -> T
    39 end;
    39 end;
    40 
    40 
    41 structure Facts: FACTS =
    41 structure Facts: FACTS =
   190 
   190 
   191 (* add static entries *)
   191 (* add static entries *)
   192 
   192 
   193 fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   193 fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   194   let
   194   let
   195     val (name, facts') = if Binding.is_nothing b then ("", facts)
   195     val (name, facts') = if Binding.is_empty b then ("", facts)
   196       else let
   196       else let
   197         val (space, tab) = facts;
   197         val (space, tab) = facts;
   198         val (name, space') = NameSpace.declare_binding naming b space;
   198         val (name, space') = NameSpace.declare naming b space;
   199         val entry = (name, (Static ths, serial ()));
   199         val entry = (name, (Static ths, serial ()));
   200         val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   200         val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   201           handle Symtab.DUP dup => err_dup_fact dup;
   201           handle Symtab.DUP dup => err_dup_fact dup;
   202       in (name, (space', tab')) end;
   202       in (name, (space', tab')) end;
   203     val props' =
   203     val props' =
   211 
   211 
   212 (* add dynamic entries *)
   212 (* add dynamic entries *)
   213 
   213 
   214 fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
   214 fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
   215   let
   215   let
   216     val (name, space') = NameSpace.declare_binding naming b space;
   216     val (name, space') = NameSpace.declare naming b space;
   217     val entry = (name, (Dynamic f, serial ()));
   217     val entry = (name, (Dynamic f, serial ()));
   218     val tab' = Symtab.update_new entry tab
   218     val tab' = Symtab.update_new entry tab
   219       handle Symtab.DUP dup => err_dup_fact dup;
   219       handle Symtab.DUP dup => err_dup_fact dup;
   220   in (name, make_facts (space', tab') props) end;
   220   in (name, make_facts (space', tab') props) end;
   221 
   221