src/HOL/Tools/typedef_package.ML
changeset 12694 9950c1ce9d24
parent 12624 9ed65232429c
child 12876 a70df1e5bf10
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Jan 10 01:10:58 2002 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Jan 10 01:11:43 2002 +0100
     1.3 @@ -247,8 +247,8 @@
     1.4        prepare_typedef prep_term true name typ set opt_morphs thy;
     1.5      val att = #1 o att_result;
     1.6    in
     1.7 -    thy |> IsarThy.theorem_i Drule.internalK (None, [])
     1.8 -      ((("", [att]), (goal, ([goal_pat], []))), comment) int
     1.9 +    thy
    1.10 +    |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
    1.11    end;
    1.12  
    1.13  val typedef_proof = gen_typedef_proof read_term;