equal
deleted
inserted
replaced
46 val retrieve = Item_Net.retrieve o Rules.get o Context.Proof; |
46 val retrieve = Item_Net.retrieve o Rules.get o Context.Proof; |
47 val retrieve_global = Item_Net.retrieve o Rules.get o Context.Theory; |
47 val retrieve_global = Item_Net.retrieve o Rules.get o Context.Theory; |
48 |
48 |
49 fun add class (ts, ths) lthy = |
49 fun add class (ts, ths) lthy = |
50 let |
50 let |
51 val cts = map (Thm.cterm_of (ProofContext.theory_of lthy)) ts; |
51 val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts; |
52 in |
52 in |
53 lthy |> Local_Theory.declaration true |
53 lthy |> Local_Theory.declaration true |
54 (fn phi => |
54 (fn phi => |
55 let |
55 let |
56 val (ts', ths') = |
56 val (ts', ths') = |