1.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 12 09:00:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Aug 12 20:11:13 2010 +0800
     1.3 @@ -101,7 +101,6 @@
     1.4      rtac rep_inj]) 1
     1.5  end
     1.6  
     1.7 -
     1.8  (* proves the quot_type theorem for the new type *)
     1.9  fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
    1.10  let
    1.11 @@ -114,25 +113,6 @@
    1.12      (K (typedef_quot_type_tac equiv_thm typedef_info))
    1.13  end
    1.14  
    1.15 -(* proves the quotient theorem for the new type *)
    1.16 -fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
    1.17 -let
    1.18 -  val quotient_const = Const (@{const_name "Quotient"}, dummyT)
    1.19 -  val goal =
    1.20 -    HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
    1.21 -    |> Syntax.check_term lthy
    1.22 -
    1.23 -  val typedef_quotient_thm_tac =
    1.24 -    EVERY1 [
    1.25 -      K (rewrite_goals_tac [abs_def, rep_def]),
    1.26 -      rtac @{thm quot_type.Quotient},
    1.27 -      rtac quot_type_thm]
    1.28 -in
    1.29 -  Goal.prove lthy [] [] goal
    1.30 -    (K typedef_quotient_thm_tac)
    1.31 -end
    1.32 -
    1.33 -
    1.34  (* main function for constructing a quotient type *)
    1.35  fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
    1.36  let
    1.37 @@ -160,15 +140,17 @@
    1.38    val abs_name = Binding.prefix_name "abs_" qty_name
    1.39    val rep_name = Binding.prefix_name "rep_" qty_name
    1.40  
    1.41 -  val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
    1.42 -  val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
    1.43 +  val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
    1.44 +  val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
    1.45  
    1.46    (* quot_type theorem *)
    1.47    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
    1.48  
    1.49    (* quotient theorem *)
    1.50 -  val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
    1.51    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
    1.52 +  val quotient_thm = 
    1.53 +    (quot_thm RS @{thm quot_type.Quotient})
    1.54 +    |> fold_rule [abs_def, rep_def]
    1.55  
    1.56    (* name equivalence theorem *)
    1.57    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name