src/HOL/Statespace/distinct_tree_prover.ML

 (* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
  * the right hand sides of insts
  *)
 fun instantiate instTs insts =
   let
-    val instTs' = map (fn (T, U) => (dest_TVar (typ_of T), typ_of U)) instTs;
+    val instTs' = map (fn (T, U) => (dest_TVar (Thm.typ_of T), Thm.typ_of U)) instTs;
     fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
     fun mapT_and_recertify ct =
       let
-        val thy = theory_of_cterm ct;
-      in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
+        val thy = Thm.theory_of_cterm ct;
+      in (Thm.cterm_of thy (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct))) end;
     val insts' = map (apfst mapT_and_recertify) insts;
   in Thm.instantiate (instTs, insts') end;
 
 fun tvar_clash ixn S S' =
   raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []);

 fun naive_cterm_first_order_match (t, ct) env =
   let
     fun mtch (env as (tyinsts, insts)) =
       fn (Var (ixn, T), ct) =>
           (case AList.lookup (op =) insts ixn of
-            NONE => (naive_typ_match (T, typ_of (ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
+            NONE =>
+              (naive_typ_match (T, Thm.typ_of (Thm.ctyp_of_term ct)) tyinsts, (ixn, ct) :: insts)
           | SOME _ => env)
        | (f $ t, ct) =>
           let val (cf, ct') = Thm.dest_comb ct;
           in mtch (mtch env (f, cf)) (t, ct') end
        | _ => env;
   in mtch env (t, ct) end;
 
 
 fun discharge prems rule =
   let
-    val thy = theory_of_thm (hd prems);
+    val thy = Thm.theory_of_thm (hd prems);
     val (tyinsts,insts) =
-      fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([], []);
+      fold naive_cterm_first_order_match (Thm.prems_of rule ~~ map Thm.cprop_of prems) ([], []);
 
     val tyinsts' =
-      map (fn (v, (S, U)) => (ctyp_of thy (TVar (v, S)), ctyp_of thy U)) tyinsts;
+      map (fn (v, (S, U)) =>
+        (Thm.ctyp_of thy (TVar (v, S)), Thm.ctyp_of thy U)) tyinsts;
     val insts' =
-      map (fn (idxn, ct) => (cterm_of thy (Var (idxn, typ_of (ctyp_of_term ct))), ct)) insts;
+      map (fn (idxn, ct) =>
+        (Thm.cterm_of thy (Var (idxn, Thm.typ_of (Thm.ctyp_of_term ct))), ct)) insts;
     val rule' = Thm.instantiate (tyinsts', insts') rule;
   in fold Thm.elim_implies prems rule' end;
 
 local
 
 val (l_in_set_root, x_in_set_root, r_in_set_root) =
   let
     val (Node_l_x_d, r) =
-      cprop_of @{thm in_set_root}
+      Thm.cprop_of @{thm in_set_root}
       |> Thm.dest_comb |> #2
       |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
     val (Node_l, x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
     val l = Node_l |> Thm.dest_comb |> #2;
   in (l,x,r) end;
 
 val (x_in_set_left, r_in_set_left) =
   let
     val (Node_l_x_d, r) =
-      cprop_of @{thm in_set_left}
+      Thm.cprop_of @{thm in_set_left}
       |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
       |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
     val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
   in (x, r) end;
 
 val (x_in_set_right, l_in_set_right) =
   let
     val (Node_l, x) =
-      cprop_of @{thm in_set_right}
+      Thm.cprop_of @{thm in_set_right}
       |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
       |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
       |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1
       |> Thm.dest_comb;
     val l = Node_l |> Thm.dest_comb |> #2;

             (case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right})
          in dist_subtree ps (discharge [thm] rule) end;
 
     val (ps, x_rest, y_rest) = split_common_prefix x_path y_path;
     val dist_subtree_thm = dist_subtree ps dist_thm;
-    val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
+    val subtree = Thm.cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
     val (_, [l, _, _, r]) = Drule.strip_comb subtree;
 
     fun in_set ps tree =
       let
         val (_, [l, x, _, r]) = Drule.strip_comb tree;
-        val xT = ctyp_of_term x;
+        val xT = Thm.ctyp_of_term x;
       in
         (case ps of
           [] =>
             instantiate
-              [(ctyp_of_term x_in_set_root, xT)]
+              [(Thm.ctyp_of_term x_in_set_root, xT)]
               [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root}
         | Left :: ps' =>
             let
               val in_set_l = in_set ps' l;
               val in_set_left' =
                 instantiate
-                  [(ctyp_of_term x_in_set_left, xT)]
+                  [(Thm.ctyp_of_term x_in_set_left, xT)]
                   [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left};
             in discharge [in_set_l] in_set_left' end
         | Right :: ps' =>
             let
               val in_set_r = in_set ps' r;
               val in_set_right' =
                 instantiate
-                  [(ctyp_of_term x_in_set_right, xT)]
+                  [(Thm.ctyp_of_term x_in_set_right, xT)]
                   [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right};
             in discharge [in_set_r] in_set_right' end)
       end;
 
   fun in_set' [] = raise TERM ("distinctTreeProver", [])

     let
       val ct =
         @{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
         |> Thm.dest_comb |> #2;
       val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
-    in (alpha, #1 (dest_Var (term_of ct))) end;
+    in (alpha, #1 (dest_Var (Thm.term_of ct))) end;
 in
 
 fun subtractProver (Const (@{const_name Tip}, T)) ct dist_thm =
       let
         val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
-        val thy = theory_of_cterm ct;
+        val thy = Thm.theory_of_cterm ct;
         val [alphaI] = #2 (dest_Type T);
       in
         Thm.instantiate
-          ([(alpha, ctyp_of thy alphaI)],
-           [(cterm_of thy (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip}
+          ([(alpha, Thm.ctyp_of thy alphaI)],
+           [(Thm.cterm_of thy (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip}
       end
   | subtractProver (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm =
       let
         val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
         val (_, [cl, _, _, cr]) = Drule.strip_comb ct;
-        val ps = the (find_tree x (term_of ct'));
+        val ps = the (find_tree x (Thm.term_of ct'));
         val del_tree = deleteProver dist_thm ps;
         val dist_thm' = discharge [del_tree, dist_thm] @{thm delete_Some_all_distinct};
-        val sub_l = subtractProver (term_of cl) cl (dist_thm');
+        val sub_l = subtractProver (Thm.term_of cl) cl (dist_thm');
         val sub_r =
-          subtractProver (term_of cr) cr
+          subtractProver (Thm.term_of cr) cr
             (discharge [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res});
       in discharge [del_tree, sub_l, sub_r] @{thm subtract_Node} end;
 
 end;
 
 fun distinct_implProver dist_thm ct =
   let
     val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
-    val sub = subtractProver (term_of ctree) ctree dist_thm;
+    val sub = subtractProver (Thm.term_of ctree) ctree dist_thm;
   in @{thm subtract_Some_all_distinct} OF [sub, dist_thm] end;
 
 fun get_fst_success f [] = NONE
   | get_fst_success f (x :: xs) =
       (case f x of

       | SOME v => SOME v);
 
 fun neq_x_y ctxt x y name =
   (let
     val dist_thm = the (try (Proof_Context.get_thm ctxt) name);
-    val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
-    val tree = term_of ctree;
+    val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
+    val tree = Thm.term_of ctree;
     val x_path = the (find_tree x tree);
     val y_path = the (find_tree y tree);
     val thm = distinctTreeProver dist_thm x_path y_path;
   in SOME thm
   end handle Option.Option => NONE);