--- a/src/HOL/Tools/Function/function_common.ML Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Fri Mar 06 13:39:34 2015 +0100
@@ -325,9 +325,9 @@
elims = Option.map (map fact) elims, pelims = map fact pelims }
end
-fun lift_morphism thy f =
+fun lift_morphism ctxt f =
let
- fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t))
+ fun term t = Thm.term_of (Drule.cterm_rule f (Proof_Context.cterm_of ctxt t))
in
Morphism.morphism "lift_morphism"
{binding = [],
@@ -338,13 +338,12 @@
fun import_function_data t ctxt =
let
- val thy = Proof_Context.theory_of ctxt
- val ct = Thm.cterm_of thy t
- val inst_morph = lift_morphism thy o Thm.instantiate
+ val ct = Proof_Context.cterm_of ctxt t
+ val inst_morph = lift_morphism ctxt o Thm.instantiate
fun match (trm, data) =
- SOME (transform_function_data data (inst_morph (Thm.match (Thm.cterm_of thy trm, ct))))
- handle Pattern.MATCH => NONE
+ SOME (transform_function_data data (inst_morph (Thm.match (Proof_Context.cterm_of ctxt trm, ct))))
+ handle Pattern.MATCH => NONE
in
get_first match (Item_Net.retrieve (get_functions ctxt) t)
end