125 struct |
125 struct |
126 |
126 |
127 fun legacy_unvarifyT thm = |
127 fun legacy_unvarifyT thm = |
128 let |
128 let |
129 val cT = Thm.ctyp_of (Thm.theory_of_thm thm); |
129 val cT = Thm.ctyp_of (Thm.theory_of_thm thm); |
130 val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (Drule.tvars_of thm); |
130 val tvars = rev (Drule.fold_terms Term.add_tvars thm []); |
|
131 val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars; |
131 in Drule.instantiate' tfrees [] thm end; |
132 in Drule.instantiate' tfrees [] thm end; |
132 |
133 |
133 fun legacy_unvarify raw_thm = |
134 fun legacy_unvarify raw_thm = |
134 let |
135 let |
135 val thm = legacy_unvarifyT raw_thm; |
136 val thm = legacy_unvarifyT raw_thm; |
136 val ct = Thm.cterm_of (Thm.theory_of_thm thm); |
137 val ct = Thm.cterm_of (Thm.theory_of_thm thm); |
137 val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (Drule.vars_of thm); |
138 val vars = rev (Drule.fold_terms Term.add_vars thm []); |
|
139 val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars; |
138 in Drule.instantiate' [] frees thm end; |
140 in Drule.instantiate' [] frees thm end; |
|
141 |
139 |
142 |
140 (** locale elements and expressions **) |
143 (** locale elements and expressions **) |
141 |
144 |
142 datatype ctxt = datatype Element.ctxt; |
145 datatype ctxt = datatype Element.ctxt; |
143 |
146 |
864 |
867 |
865 local |
868 local |
866 |
869 |
867 fun axioms_export axs _ hyps = |
870 fun axioms_export axs _ hyps = |
868 Element.satisfy_thm axs |
871 Element.satisfy_thm axs |
869 #> Drule.implies_intr_list (Library.drop (length axs, hyps)) |
872 #> Drule.implies_intr_list (Library.drop (length axs, hyps)); |
870 #> Seq.single; |
|
871 |
873 |
872 |
874 |
873 (* NB: derived ids contain only facts at this stage *) |
875 (* NB: derived ids contain only facts at this stage *) |
874 |
876 |
875 fun activate_elem _ _ ((ctxt, mode), Fixes fixes) = |
877 fun activate_elem _ _ ((ctxt, mode), Fixes fixes) = |