src/CCL/Wfd.thy

             tac [((("g", 0), Position.none), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs)
   in try_IHs rnames end)
 
 fun is_rigid_prog t =
   (case (Logic.strip_assums_concl t) of
-    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem _ for a _\<close>\<close>\<close> => null (Term.add_vars a [])
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem _ for a _\<close>\<close> => null (Term.add_vars a [])
   | _ => false)
 
 in
 
 fun rcall_tac ctxt i =