src/CCL/Wfd.thy

 
 
 subsection {* Typechecking *}
 
 ML {*
-
 local
 
 val type_rls =
   @{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
   @{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};

       fun try_IHs [] = no_tac
         | try_IHs ((x,y)::xs) = tac [(("g", 0), 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(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a [])
-       | _ => false
+  (case (Logic.strip_assums_concl t) of
+    (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =>
+      null (Term.add_vars a [])
+  | _ => false)
+
 in
 
 fun rcall_tac ctxt i =
   let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i
   in IHinst tac @{thms rcallTs} i end

   rcall_tac ctxt i ORELSE
   ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
   match_tac ctxt [@{thm SubtypeI}] i
 
 fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
-          if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
+    if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
 
 fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i
 
-fun tac ctxt = typechk_tac ctxt [] 1
 
 (*** Clean up Correctness Condictions ***)
 
 fun clean_ccs_tac ctxt =
   let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in