src/Pure/facts.ML
changeset 28864 d6fe93e3dcb9
parent 27738 66596d7aa899
child 28941 128459bd72d2
equal deleted inserted replaced
28863:32e83a854e5e 28864:d6fe93e3dcb9
    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 -> string * thm list -> T -> T
    34   val add_global: NameSpace.naming -> Name.binding * thm list -> T -> string * T
    35   val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
    35   val add_local: bool -> NameSpace.naming -> Name.binding * thm list -> T -> string * T
    36   val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
    36   val add_dynamic: NameSpace.naming -> Name.binding * (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 =
   188   in make_facts facts' props' end;
   188   in make_facts facts' props' end;
   189 
   189 
   190 
   190 
   191 (* add static entries *)
   191 (* add static entries *)
   192 
   192 
   193 fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
   193 fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   194   let
   194   let
   195     val facts' =
   195     val (name, facts') = if Name.is_nothing b then ("", facts)
   196       if name = "" then facts
   196       else let
   197       else
   197         val (space, tab) = facts;
   198         let
   198         val (name, space') = NameSpace.declare_binding naming b space;
   199           val (space, tab) = facts;
   199         val entry = (name, (Static ths, serial ()));
   200           val space' = NameSpace.declare naming name space;
   200         val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   201           val entry = (name, (Static ths, serial ()));
   201           handle Symtab.DUP dup => err_dup_fact dup;
   202           val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   202       in (name, (space', tab')) end;
   203             handle Symtab.DUP dup => err_dup_fact dup;
       
   204         in (space', tab') end;
       
   205     val props' =
   203     val props' =
   206       if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   204       if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   207       else props;
   205       else props;
   208   in make_facts facts' props' end;
   206   in (name, make_facts facts' props') end;
   209 
   207 
   210 val add_global = add false false;
   208 val add_global = add false false;
   211 val add_local = add true;
   209 val add_local = add true;
   212 
   210 
   213 
   211 
   214 (* add dynamic entries *)
   212 (* add dynamic entries *)
   215 
   213 
   216 fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
   214 fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
   217   let
   215   let
   218     val space' = NameSpace.declare naming name space;
   216     val (name, space') = NameSpace.declare_binding naming b space;
   219     val entry = (name, (Dynamic f, serial ()));
   217     val entry = (name, (Dynamic f, serial ()));
   220     val tab' = Symtab.update_new entry tab
   218     val tab' = Symtab.update_new entry tab
   221       handle Symtab.DUP dup => err_dup_fact dup;
   219       handle Symtab.DUP dup => err_dup_fact dup;
   222   in make_facts (space', tab') props end;
   220   in (name, make_facts (space', tab') props) end;
   223 
   221 
   224 
   222 
   225 (* remove entries *)
   223 (* remove entries *)
   226 
   224 
   227 fun del name (Facts {facts = (space, tab), props}) =
   225 fun del name (Facts {facts = (space, tab), props}) =