diff -r ca6b4bc7a871 -r 89c55d36980f Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Dec 08 12:37:25 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 08 13:05:04 2010 +0000
@@ -113,91 +113,6 @@
 end
 *}
 
-(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or
-   appends of elements; in case of recursive calls it retruns also the applied
-   bn function *)
-ML {*
-fun strip_bn_fun lthy args t =
-let 
-  fun aux t =
-    case t of
-      Const (@{const_name sup}, _) $ l $ r => aux l @ aux r
-    | Const (@{const_name append}, _) $ l $ r => aux l @ aux r
-    | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
-        (find_index (equal x) args, NONE) :: aux y
-    | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
-        (find_index (equal x) args, NONE) :: aux y
-    | Const (@{const_name bot}, _) => []
-    | Const (@{const_name Nil}, _) => []
-    | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)]
-    | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t))
-in
-  aux t
-end  
-*}
-
-ML {*
-(** definition of the raw binding functions **)
-
-fun prep_bn_info lthy dt_names dts bn_funs eqs = 
-let
-  fun process_eq eq = 
-  let
-    val (lhs, rhs) = eq
-      |> HOLogic.dest_Trueprop
-      |> HOLogic.dest_eq
-    val (bn_fun, [cnstr]) = strip_comb lhs
-    val (_, ty) = dest_Const bn_fun
-    val (ty_name, _) = dest_Type (domain_type ty)
-    val dt_index = find_index (fn x => x = ty_name) dt_names
-    val (cnstr_head, cnstr_args) = strip_comb cnstr    
-    val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head))
-    val rhs_elements = strip_bn_fun lthy cnstr_args rhs
-  in
-    ((bn_fun, dt_index), (cnstr_name, rhs_elements))
-  end
-
-  (* order according to constructor names *)
-  fun cntrs_order ((bn, dt_index), data) = 
-  let
-    val dt = nth dts dt_index                      
-    val cts = (fn (_, _, _, x) => x) dt     
-    val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts  
-  in
-    (bn, (bn, dt_index, order (op=) ct_names data))
-  end
- 
-in
-  eqs
-  |> map process_eq 
-  |> AList.group (op=)      (* eqs grouped according to bn_functions *)
-  |> map cntrs_order        (* inner data ordered according to constructors *)
-  |> order (op=) bn_funs    (* ordered according to bn_functions *)
-end
-*}
-
-ML {*
-fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
-  if null raw_bn_funs 
-  then ([], [], [], [], lthy)
-  else 
-    let
-      val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
-        Function_Common.default_config (pat_completeness_simp constr_thms) lthy
-
-      val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1)
-      val {fs, simps, inducts, ...} = info
-
-      val raw_bn_induct = (the inducts)
-      val raw_bn_eqs = the simps
-
-      val raw_bn_info = 
-        prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)
-    in
-      (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
-    end
-
-*}
 
 ML {*
 fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
@@ -646,8 +561,8 @@
      ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
      ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)
 in
-  (0, lthy9')
-end handle TEST ctxt => (0, ctxt)
+  lthy9'
+end handle TEST ctxt => ctxt
 *}
 
 
@@ -821,7 +736,7 @@
 
   val bclauses' = complete dt_strs bclauses
 in
-  timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |> snd)
+  timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy)
 end
 *}