1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -31,8 +31,8 @@
     1.4    val no_thycontext : guh -> bool
     1.5    val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
     1.6    val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
     1.7 -  val get_tac_checked : Ctree.ptree -> Ctree.pos' -> Ctree.tac
     1.8 -  val context_thy : Ctree.ptree * Ctree.pos' -> Ctree.tac -> contthy
     1.9 +  val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac
    1.10 +  val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy
    1.11    val distinct_Thm : rule list -> rule list
    1.12    val eq_Thms : string list -> rule -> bool
    1.13    val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->