src/Pure/theory.ML
changeset 70362 421727c19b23
parent 70361 34b271c4f400
child 70923 98d9b78b7f47
equal deleted inserted replaced
70361:34b271c4f400 70362:421727c19b23
   169 val defs_of = #defs o rep_theory;
   169 val defs_of = #defs o rep_theory;
   170 
   170 
   171 
   171 
   172 (* join theory *)
   172 (* join theory *)
   173 
   173 
   174 val join_theory = foldl1 Context.join_thys;
   174 fun join_theory [] = raise List.Empty
       
   175   | join_theory [thy] = thy
       
   176   | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys);
   175 
   177 
   176 
   178 
   177 (* begin/end theory *)
   179 (* begin/end theory *)
   178 
   180 
   179 val begin_wrappers = rev o #1 o #wrappers o rep_theory;
   181 val begin_wrappers = rev o #1 o #wrappers o rep_theory;