diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/rewtools.sml
--- a/src/Tools/isac/Interpret/rewtools.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -31,8 +31,8 @@
   val no_thycontext : guh -> bool
   val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
   val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
-  val get_tac_checked : Ctree.ptree -> Ctree.pos' -> Ctree.tac
-  val context_thy : Ctree.ptree * Ctree.pos' -> Ctree.tac -> contthy
+  val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac
+  val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy
   val distinct_Thm : rule list -> rule list
   val eq_Thms : string list -> rule -> bool
   val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->