equal
deleted
inserted
replaced
171 |
171 |
172 |
172 |
173 fun mk_free ctxt name = |
173 fun mk_free ctxt name = |
174 if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name |
174 if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name |
175 then |
175 then |
176 let val n' = Variable.intern_fixed ctxt name |
176 let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden; |
177 in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end |
177 in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end |
178 else NONE |
178 else NONE |
179 |
179 |
180 |
180 |
181 fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name; |
181 fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name; |