equal
deleted
inserted
replaced
74 end; |
74 end; |
75 |
75 |
76 in |
76 in |
77 |
77 |
78 val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars; |
78 val bundle = gen_bundle (K I) (K I) Proof_Context.cert_vars; |
79 val bundle_cmd = |
79 val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.read_vars; |
80 gen_bundle Proof_Context.get_fact (Attrib.intern_src o Proof_Context.theory_of) |
|
81 Proof_Context.read_vars; |
|
82 |
80 |
83 end; |
81 end; |
84 |
82 |
85 |
83 |
86 (* include bundles *) |
84 (* include bundles *) |