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 (Proof_Context.cterm_of lthy) ts; |
51 val cts = map (Thm.cterm_of lthy) ts; |
52 in |
52 in |
53 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
53 lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
54 (fn phi => |
54 (fn phi => |
55 let |
55 let |
56 val (ts', ths') = |
56 val (ts', ths') = |