src/Pure/Isar/object_logic.ML
changeset 74340 e098fa45bfe0
parent 70471 1004333b76aa
child 74341 edf8b141a8c4
equal deleted inserted replaced
74339:bff865939cc3 74340:e098fa45bfe0
    89 
    89 
    90 fun gen_add_judgment add_consts (b, T, mx) thy =
    90 fun gen_add_judgment add_consts (b, T, mx) thy =
    91   let
    91   let
    92     val c = Sign.full_name thy b;
    92     val c = Sign.full_name thy b;
    93     val thy' = thy |> add_consts [(b, T, mx)];
    93     val thy' = thy |> add_consts [(b, T, mx)];
    94     val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c);
       
    95   in
    94   in
    96     thy'
    95     thy'
    97     |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) []
    96     |> Theory.add_deps_const c
    98     |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
    97     |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
    99         if is_some judgment then error "Attempt to redeclare object-logic judgment"
    98         if is_some judgment then error "Attempt to redeclare object-logic judgment"
   100         else (base_sort, SOME c, atomize_rulify))
    99         else (base_sort, SOME c, atomize_rulify))
   101   end;
   100   end;
   102 
   101